case mp =>
  intro (_ : Negative (n——m))
  show n < m
  apply Natural.lt_defn_add.mpr
  show ∃ (k : ℕ), Positive k ∧ m ≃ n + k
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ -1 * coe k))
      := Generic.negative_iff_sign_neg1.mp ‹Negative (n——m)›
  have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
  have : n + k ≃ 0 + m := ‹n——m ≃ 0——k›
  have : m ≃ n + k := calc
    m     ≃ _ := Rel.symm AA.identL
    0 + m ≃ _ := Rel.symm ‹n + k ≃ 0 + m›
    n + k ≃ _ := Rel.refl
  exact Exists.intro k (And.intro ‹Positive k› ‹m ≃ n + k›)
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m
no goals