Theorem isub_cancel_middle

Proof
isub_cancel_middle. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ →
  (a - b) + (b - c) = a - c,
  pred_iii_restr int_incl_in_real rsub_cancel_middle.

Dependencies
The given proof depends on nine axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rneg_closed.