DeZero.eq_symm

Énoncé

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

Retourne une égalité : de a = b, tire b = a.

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

/-- Symétrie de l'égalité : de `a = b` on tire `b = a`. -/
theorem eq_symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
  Eq.rec (motive := fun x _ => x = a) rfl h