blob: 89dd199b31eef8f14b08fbc6100ba56acd80a0e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
import Lean
/- This lemma is generally useful. It often happens that (because we
make a split on a condition for instance) we have `x ≠ y` in the context
and need to simplify `y ≠ x` somewhere. -/
@[simp]
theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
/- This is generally useful, and doing without is actually quite cumbersome.
Note that the following theorem does not seem to be necessary (we invert `x`
and `y` in the conclusion), probably because of `neq_imp`:
`¬ x = y → ¬ y == x`
-/
@[simp]
theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*]
|
