have : (c - b) + (b - a) ≃ c - a := calc
  (c - b) + (b - a)   ≃ _ := AA.substL sub_defn
  (c + -b) + (b - a)  ≃ _ := AA.substR sub_defn
  (c + -b) + (b + -a) ≃ _ := AA.assoc
  c + (-b + (b + -a)) ≃ _ := AA.substR (Rel.symm AA.assoc)
  c + ((-b + b) + -a) ≃ _ := AA.substR (AA.substL AA.inverseL)
  c + (0 + -a)        ≃ _ := AA.substR AA.identL
  c + -a              ≃ _ := Rel.symm sub_defn
  c - a               ≃ _ := Rel.refl
ℕ : 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)
ℕ : 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))
this : c - b + (b - a) ≃ c - a
⊢ Positive (c - a)