cas_sur

Énoncé

∀ {p : Prop} {c : Prop} (hp : p → c) (hnp : ¬p → c), c

Raisonne par cas sur une proposition quelconque : si elle est vraie, et si elle est fausse.

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

/-- Analyse de cas sur une proposition quelconque : la forme la plus utilisable du tiers exclu. -/
theorem cas_sur {p c : Prop} (hp : p → c) (hnp : ¬p → c) : c :=
  or_elim (ax8_tiers_exclu p) hp hnp

-- =============================================
-- CÂBLAGE DE `calc` SUR L'ORDRE
-- =============================================