non_non

Énoncé

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

Si nier une proposition mène à l’absurde, c’est qu’elle est vraie.

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

/-- Élimination de la double négation. -/
theorem non_non {p : Prop} (h : ¬¬p) : p :=
  par_absurde (fun hnp => h hnp)