have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
⊢ ∃ k, Positive k ∧ m ≃ n + k
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this : n——m ≃ 0——k
⊢ ∃ k, Positive k ∧ m ≃ n + k