Proof isub_neg. ⊢ a ∈ ℤ → b ∈ ℤ → -(a - b) = b - a, pred_ii_restr int_incl_in_real rsub_neg.
Dependencies
The given proof depends on 13 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.