proposition: Lemma R_is_Field2: forall (x y : RRing) (x_ : x[#][0]) (y_ : y[#][0]), Rrecip x x_[#]Rrecip y y_ -> x[#]y.
proof: Proof. intros x y x1 y1 H. intro. apply H. clear H. unfold Rrecip. rewrite H0. trivial. Qed.
imports: CoRN.algebra.CSetoids CoRN.algebra.CSemiGroups CoRN.algebra.CMonoids CoRN.algebra.CGroups CoRN.tactics.CornTac CoRN.algebra.CAbGroups CoRN.algebra.CRings CoRN.algebra.CFields CoRN.algebra.COrdFields CoRN.reals.CReals Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun Coq(Lra)