proposition: Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
proof: Proof. constructor. - intro; apply Rplus_0_l. - exact Rplus_comm. - symmetry ; apply Rplus_assoc. - intro; apply Rmult_1_l. - exact Rmult_comm. - symmetry ; apply Rmult_assoc. - intros m n p. rewrite Rmult_comm. rewrite (Rmult_comm n p). rewrite (Rmult_comm m p). apply Rmult_plus_distr_l. - reflexivity. - exact Rplus_opp_r. Qed.
imports: Nnat ArithRing Ring Field Rdefinitions Rpow_def Raxioms