case mp =>
  intro (_ : Positive (n——m))
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ 1 * coe k))
      := Generic.positive_iff_sign_pos1.mp ‹Positive (n——m)›
  show m < n
  apply neg_diff_lt.mp
  show Negative (m——n)
  apply Generic.negative_iff_sign_neg1.mpr
  show NonzeroWithSign (m——n) (-1)
  apply NonzeroWithSign.intro k ‹Positive k›
  show m——n ≃ -1 * coe k
  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 : ℕ
⊢ Positive (n——m) → n > m
no goals