grind instances for Int as an ordered module.

instance Lean.Grind.instPreorderInt : Preorder Int

Equations

• Lean.Grind.instPreorderInt = { toLE := Int.instLEInt, toLT := Int.instLTInt, le_refl := Int.le_refl, le_trans := ⋯, lt_iff_le_not_le := @Lean.Grind.instPreorderInt._proof_2 }

instance Lean.Grind.instIsOrderedInt : IntModule.IsOrdered Int

instance Lean.Grind.instIsOrderedInt_1 : Ring.IsOrdered Int