calc
  n + 0 ≃ _ := AA.identR
  n     ≃ _ := ‹n ≃ m›
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.refl
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
no goals