feat(algebra/order): ne_iff_lt_iff_le

 
 (#5731)




Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

src/algebra/order.lean

@@ -134,6 +134,9 @@ alias eq_or_lt_of_le ← has_le.le.eq_or_lt
 lemma ne.le_iff_lt [partial_order α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a < b :=
 ⟨λ h', lt_of_le_of_ne h' h, λ h, h.le⟩
 
+@[simp] lemma ne_iff_lt_iff_le [partial_order α] {a b : α} : (a ≠ b ↔ a < b) ↔ a ≤ b :=
+⟨λ h, classical.by_cases le_of_eq (le_of_lt ∘ h.mp), λ h, ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩
+
 lemma lt_of_not_ge' [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
 ((le_total _ _).resolve_right h).lt_of_not_le h
 

src/data/buffer/parser/basic.lean

@@ -36,32 +36,6 @@ For some `parse_result α`, give the position at which the result was provided,
 | (done n _) := n
 | (fail n _) := n
 
-section lemmas
-
--- TODO: place in relevant files
-
-variables {α : Type*} {P Q : α → Prop} {Q' : Prop} {x : α}
-
-@[simp] lemma ne_iff_lt_iff_le {n m : ℕ} : (n ≠ m ↔ n < m) ↔ n ≤ m :=
-begin
-  refine ⟨λ h, _, λ h, _⟩,
-  { by_cases H : n = m,
-    { exact le_of_eq H },
-    { exact le_of_lt (h.mp H) } },
-  { rcases eq_or_lt_of_le h with rfl|H,
-    { simp },
-    { simp [H, ne_of_lt] } }
-end
-
-lemma nat.le_of_sub_eq_pos {m n k : ℕ} (h : m - n = k) (hk : 0 < k) : n ≤ m :=
-begin
-  contrapose! hk,
-  rw nat.sub_eq_zero_of_le (le_of_lt hk) at h,
-  rw h
-end
-
-end lemmas
-
 namespace parser
 
 section defn_lemmas