DeZero.eq_trans

Énoncé

∀ {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b = c), a = c

Enchaîne deux égalités : de a = b et b = c, tire a = c.

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

/-- Transitivité de l'égalité : c'est le bloc que le nœud `calc` empilera. -/
theorem eq_trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
  Eq.rec (motive := fun x _ => a = x) h₁ h₂