apply Natural.lt_defn_add.mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ n < m
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ ∃ k, Positive k ∧ m ≃ n + k