apply Iff.intro
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 ↔ (n——m).sgn ≃ 0
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → (n——m).sgn ≃ 0

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 0 → n——m ≃ 0