proposition: Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
proof: Proof. constructor. - exact RTheory. - exact R1_neq_R0. - reflexivity. - exact Rinv_l. Qed.
imports: Nnat ArithRing Ring Field Rdefinitions Rpow_def Raxioms