theorem Ord.toLE_opposite_eq {α : Type u_1} [ord : Ord α] (a b : α) : a ≤ b ↔ b ≤ a

theorem Ord.toLT_opposite_eq {α : Type u_1} [ord : Ord α] (a b : α) : a < b ↔ b < a

@[simp]

theorem Ord.toLT_iff_opposite {α : Type u_1} [ord : Ord α] (lt_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a