proposition: Lemma RringExt : ring_eq_ext Rplus Rmult Ropp Req_constr.
proof: Proof. split. - intros x y H z t H0. apply Req_constr_leibniz in H. apply Req_constr_leibniz in H0. destruct H, H0. apply Req_constr_refl. - intros x y H z t H0. apply Req_constr_leibniz in H. apply Req_constr_leibniz in H0. destruct H, H0. apply Req_constr_refl. - intros x y H. apply Req_constr_leibniz in H. destruct H. apply Req_constr_refl. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms