have
  (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : m——n ≃ -1 * coe k))
    := Generic.negative_iff_sign_neg1.mp ‹Negative (m——n)›
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
⊢ NonzeroWithSign (n——m) 1
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ NonzeroWithSign (n——m) 1