have : Positive ((c - b) + (b - a)) :=
  add_preserves_positive ‹Positive (c - b)› ‹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
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ Positive (c - 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
x✝ : b < c
this✝¹ : Positive (b - a)
this✝ : Positive (c - b)
this : Positive (c - b + (b - a))
⊢ Positive (c - a)