proposition: Lemma CRmult_comm (x y: CR): x * y == y * x.
proof: Proof. pose (Qpos_max (CR_b (1#1) x) (CR_b (1#1) y)) as b. assert (' (- ` b)%Q <= x) as xlower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) x))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat, Qpos_max_ub_l. } assert (x <= '(` b)%Q) as xupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) x))) _ (CR_b_upperBound _ _)). apply CRle_Qle. apply Qpos_max_ub_l. } assert (' (- ` b)%Q <= y) as ylower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) y))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat, Qpos_max_ub_r. } assert (y <= '(` b)%Q) as yupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) y))) _ (CR_b_upperBound _ _)). apply CRle_Qle. apply Qpos_max_ub_r. } rewrite <- (@CRmult_bounded_mult b x y). 2: exact ylower. 2: exact yupper. rewrite <- (@CRmult_bounded_mult b y x). 2: exact xlower. 2: exact xupper. - apply CRmult_comm_bounded. + exact xlower. + exact xupper. + exact ylower. + exact yupper. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders