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