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

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