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