Theorem rsq_is_zero_impl

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 1 ⊢ ¬a = 0 → ¬a⋅a = 0, rsq_non_zero 1.
03. 1 ⊢ a⋅a = 0 → a = 0, contraposition_rev 2.
rsq_is_zero_impl. ⊢ a ∈ ℝ → a⋅a = 0 → a = 0,
  subj_intro 3.

Dependencies
The given proof depends on 17 axioms:
efq, eq_refl, eq_subst, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rinv_closed, rmul_assoc, rmul_closed, rmul_comm, rmul_distl_add, rmul_inv, rmul_neutr, rneg_closed.