have neg_diff {k : ℕ} : 0——k ≃ -1 * coe k := by
  apply Rel.symm
  calc
    (-1) * coe k ≃ _ := Rel.refl
    (-1) * k——0  ≃ _ := mul_neg_one
    (-(k——0))    ≃ _ := Rel.refl
    0——k         ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ n < m
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) ↔ n < m