Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. ⊢ a - a = a + (-a), rsub_eq. 03. 1 ⊢ a + (-a) = 0, radd_inv 1. 04. 1 ⊢ a - a = 0, eq_trans 2 3. rsub_self. ⊢ a ∈ ℝ → a - a = 0, subj_intro 4.
Dependencies
The given proof depends on three axioms:
eq_refl, eq_subst, radd_inv.