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