DeZero.and_right

Énoncé

∀ {a : Prop} {b : Prop} (h : a ∧ b), b

D’une conjonction, ne retient que sa moitié droite.

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

/-- Projection droite. -/
theorem and_right {a b : Prop} (h : a ∧ b) : b :=
  And.rec (motive := fun _ => b) (fun _ hb => hb) h