apply neg_diff_lt.mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m < n
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ Negative (m——n)