have : c + b - (c + a) ≃ b - a := calc
  c + b - (c + a) ≃ _ := AA.substL AA.comm
  b + c - (c + a) ≃ _ := AA.substR AA.comm
  b + c - (a + c) ≃ _ := sub_sums_sameR
  b - 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✝ : c + a < c + b
this : Positive (c + b - (c + a))
⊢ 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✝ : c + a < c + b
this✝ : Positive (c + b - (c + a))
this : c + b - (c + a) ≃ b - a
⊢ Positive (b - a)