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

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n > m → Positive (n——m)