DeZero.or_inr

Énoncé

∀ {a : Prop} {b : Prop} (hb : b), a ∨ b

Une preuve de b suffit à établir a ∨ b.

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

/-- Injection droite. -/
theorem or_inr {a b : Prop} (hb : b) : a ∨ b :=
  Or.inr hb