case mpr =>
  intro (_ : n ≃ m)
  show n + 0 ≃ 0 + m
  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 : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m
no goals