Theorem isub_self

Proof
isub_self. ⊢ a ∈ ℤ → a - a = 0,
  pred_restr int_incl_in_real rsub_self.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, radd_inv.