proposition: Lemma Rring : ring_theory (IQR 0) (IQR 1) Rplus Rmult (fun x y : R => (x + - y)%R) Ropp Req_constr.
proof: Proof. split. - intro x. replace (IQR 0 + x) with x. + apply Req_constr_refl. + apply Rquot1. rewrite Rrepr_plus. unfold IQR. rewrite Rquot2. rewrite CReal_plus_0_l. reflexivity. - intros. replace (x + y) with (y + x). + apply Req_constr_refl. + apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm. - intros. replace (x + (y + z)) with (x + y + z). + apply Req_constr_refl. + apply Rquot1. do 4 rewrite Rrepr_plus. apply CReal_plus_assoc. - intro x. replace (IQR 1 * x) with x. + apply Req_constr_refl. + unfold IQR. apply Rquot1. rewrite Rrepr_mult, Rquot2, CReal_mult_1_l. reflexivity. - intros. replace (x * y) with (y * x). + apply Req_constr_refl. + apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm. - intros. replace (x * (y * z)) with (x * y * z). + apply Req_constr_refl. + apply Rquot1. do 4 rewrite Rrepr_mult. apply CReal_mult_assoc. - intros. replace ((x + y) * z) with (x * z + y * z). + apply Req_constr_refl. + apply Rquot1. rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult. symmetry. apply CReal_mult_plus_distr_r. - intros. apply Req_constr_refl. - intros. replace (x + - x) with R0. + unfold IQR. rewrite R0_def. apply Req_constr_refl. + apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, CReal_plus_opp_r, Rrepr_0. reflexivity. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms