feat: has_le.le.not_lt_iff_eq (#768)

Matches leanprover-community/mathlib3#17734

Author: YaelDillies

Mathlib/Order/Basic.lean

@@ -219,11 +219,18 @@ namespace LE.le
 protected theorem ge [LE α] {x y : α} (h : x ≤ y) : y ≥ x :=
   h
 
-theorem lt_iff_ne [PartialOrder α] {x y : α} (h : x ≤ y) : x < y ↔ x ≠ y :=
-  ⟨fun h ↦ h.ne, h.lt_of_ne⟩
+section partial_order
+variable [PartialOrder α] {a b : α}
+
+lemma lt_iff_ne (h : a ≤ b) : a < b ↔ a ≠ b := ⟨fun h ↦ h.ne, h.lt_of_ne⟩
+lemma gt_iff_ne (h : a ≤ b) : a < b ↔ b ≠ a := ⟨fun h ↦ h.ne.symm, h.lt_of_ne'⟩
+lemma not_lt_iff_eq (h : a ≤ b) : ¬ a < b ↔ a = b := h.lt_iff_ne.not_left
+lemma not_gt_iff_eq (h : a ≤ b) : ¬ a < b ↔ b = a := h.gt_iff_ne.not_left
+
+lemma le_iff_eq (h : a ≤ b) : b ≤ a ↔ b = a := ⟨fun h' ↦ h'.antisymm h, Eq.le⟩
+lemma ge_iff_eq (h : a ≤ b) : b ≤ a ↔ a = b := ⟨h.antisymm, Eq.ge⟩
 
-theorem le_iff_eq [PartialOrder α] {x y : α} (h : x ≤ y) : y ≤ x ↔ y = x :=
-  ⟨fun h' ↦ h'.antisymm h, Eq.le⟩
+end partial_order
 
 theorem lt_or_le [LinearOrder α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
   ((lt_or_ge a c).imp id) fun hc ↦ le_trans hc h