class Std.LawfulOrderOrd (α : Type u) [Ord α] [LE α] : Prop

This typeclass states that the synthesized Ord α instance is compatible with the LE α instance. This means that according to compare, the following are equivalent:

• a is less than or equal to b according to compare.
• b is greater than or equal to b according to compare.
• a ≤ b holds.

LawfulOrderOrd α automatically entails that Ord α is oriented (see OrientedOrd α) and that LE α is total.

Ord α and LE α mutually determine each other in the presence of LawfulOrderOrd α.

• isLE_compare (a b : α) : (compare a b).isLE = true ↔ a ≤ b
• isGE_compare (a b : α) : (compare a b).isGE = true ↔ b ≤ a

theorem Std.LawfulOrderOrd.isLE_compare_eq_false {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} : (compare a b).isLE = false ↔ ¬a ≤ b

theorem Std.LawfulOrderOrd.isGE_compare_eq_false {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} : (compare a b).isGE = false ↔ ¬b ≤ a