calc
  n——m              ≃ _ := Rel.symm neg_involutive
  (-(-(n——m)))      ≃ _ := Rel.refl
  (-(m——n))         ≃ _ := AA.subst₁ ‹m——n ≃ -1 * coe k›
  (-(-1 * coe k))   ≃ _ := AA.subst₁ (Rel.symm AA.scompatL)
  (-(-(1 * coe k))) ≃ _ := neg_involutive
  1 * coe k         ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ n——m ≃ 1 * coe k
no goals