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