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