calc
  (-1) * coe k ≃ _ := Rel.refl
  (-1) * k——0  ≃ _ := mul_neg_one
  (-(k——0))    ≃ _ := Rel.refl
  0——k         ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ -1 * coe k ≃ 0——k
no goals