DeZero.ne_elim

Énoncé

∀ {α : Sort u} {a : α} {b : α} {c : Prop} (h : a = b) (hn : a ≠ b), c

Une égalité et sa négation se contredisent : tout en découle.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Une égalité et sa négation sont contradictoires. -/
theorem ne_elim {α : Sort u} {a b : α} {c : Prop} (h : a = b) (hn : a ≠ b) : c :=
  false_elim (hn h)