DeZero.absurde

Énoncé

∀ {a : Prop} {c : Prop} (ha : a) (hna : ¬a), c

D’une proposition et de sa négation, on tire n’importe quelle conclusion.

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

/-- D'une proposition et de sa négation on tire n'importe quelle proposition. -/
theorem absurde {a c : Prop} (ha : a) (hna : ¬a) : c :=
  false_elim (hna ha)