have : n + 0 ≃ 0 + m := ‹n——m ≃ 0——0›
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n——m ≃ 0——0
⊢ n ≃ m
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n——m ≃ 0——0
this : n + 0 ≃ 0 + m
⊢ n ≃ m