case mpr =>
  intro (_ : Positive (a - b))
  show b < a
  have
    (Exists.intro (k : ℕ) (And.intro (_ : Positive k) (_ : a - b ≃ coe k)))
      := positive_elim_nat ‹Positive (a - b)›
  apply lt_iff_le_neqv.mpr
  show b ≤ a ∧ b ≄ a
  have : a ≃ b + coe k := subR_moveR_addL.mp ‹a - b ≃ coe k›
  have : b ≤ a := le_iff_add_nat.mpr (Exists.intro k ‹a ≃ b + coe k›)
  have : k ≄ 0 := Signed.positive_defn.mp ‹Positive k›
  have : (k:ℤ) ≄ ((0:ℕ):ℤ) := AA.subst₁ ‹k ≄ 0›
  have : a - b ≄ 0 :=
    AA.neqv_substL (Rel.symm ‹a - b ≃ coe k›) ‹(coe k : ℤ) ≄ 0›
  have : b ≄ a := Rel.symm (mt zero_diff_iff_eqv.mpr ‹a - b ≄ 0›)
  exact And.intro ‹b ≤ a› ‹b ≄ a›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b
no goals