case mpr =>
  intro (_ : m < n)
  show Positive (n——m)
  apply Generic.positive_iff_sign_pos1.mpr
  show NonzeroWithSign (n——m) 1
  have : Negative (m——n) := neg_diff_lt.mpr ‹m < n›
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : m——n ≃ -1 * coe k))
      := Generic.negative_iff_sign_neg1.mp ‹Negative (m——n)›
  apply NonzeroWithSign.intro k ‹Positive k›
  show n——m ≃ 1 * coe k
  calc
    n——m              ≃ _ := Rel.symm neg_involutive
    (-(-(n——m)))      ≃ _ := Rel.refl
    (-(m——n))         ≃ _ := AA.subst₁ ‹m——n ≃ -1 * coe k›
    (-(-1 * coe k))   ≃ _ := AA.subst₁ (Rel.symm AA.scompatL)
    (-(-(1 * coe k))) ≃ _ := neg_involutive
    1 * coe k         ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n > m → Positive (n——m)
no goals