exact AA.substFn ‹b - a ≃ b + c - (a + c)› ‹Positive (b - a)›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this✝ : Positive (b - a)
this : b - a ≃ b + c - (a + c)
⊢ Positive (b + c - (a + c))
no goals