par_absurde

Énoncé

∀ {p : Prop} (h : ¬p → False), p

Pour démontrer p, il suffit que sa négation mène à l’absurde.

Axiomes consommés

Cet énoncé dépend de 1 axiome, et d’aucun autre. La liste est relevée par le noyau lui-même (#print axioms), pas déclarée à la main.

• ax8_tiers_exclu

Code

/-- Raisonnement par l'absurde : pour démontrer `p`, il suffit que `¬p` mène à une contradiction. -/
theorem par_absurde {p : Prop} (h : ¬p → False) : p :=
  or_elim (ax8_tiers_exclu p) (fun hp => hp) (fun hnp => false_elim (h hnp))