case mp =>
  intro (_ : n——m ≃ 0)
  show n ≃ m
  have : n——m ≃ 0——0 := ‹n——m ≃ 0›
  have : n + 0 ≃ 0 + m := ‹n——m ≃ 0——0›
  exact Natural.add_swapped_zeros_eqv.mp ‹n + 0 ≃ 0 + m›
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → n ≃ m
no goals