proposition: Lemma CRmult_assoc (x y z : CR): (x * y) * z == x * (y * z).
proof: Proof. pose ((CR_b (1#1) x + (1#1)) * (CR_b (1#1) y + (1#1)) * (CR_b (1#1) z + (1#1)))%Qpos as b. assert (' (- ` b)%Q <= z) as zlower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) z))%Q)). 2: apply CR_b_lowerBound. apply CRle_Qle. apply Qopp_le_compat. apply (Qle_trans _ (` (CR_b (1#1)%Qpos z) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_zfactor_le. } assert (z <= ' (` b)%Q) as zupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) z))%Q)). apply CR_b_upperBound. apply CRle_Qle. apply (Qle_trans _ (` (CR_b (1#1)%Qpos z) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_zfactor_le. } rewrite <- (@CRmult_bounded_mult b x y), <- (@CRmult_bounded_mult b). 2: exact zlower. 2: exact zupper. rewrite <- (@CRmult_bounded_mult b), <- (@CRmult_bounded_mult b). apply CRmult_assoc_bounded. - exact zlower. - exact zupper. - apply (@CRle_trans _ ('(-proj1_sig ((CR_b (1#1) y) * CR_b (1#1) z)%Qpos)%Q)). 2: apply CR_b_lowerBound_2. apply CRle_Qle, Qopp_le_compat. apply (Qle_trans _ ((1#1)*proj1_sig (CR_b (1#1) y + (1#1))%Qpos * proj1_sig ((CR_b (1#1) z) + (1#1))%Qpos)). rewrite Qmult_1_l. apply (Qpos_mult_le_compat (CR_b (1#1) y) (CR_b (1#1) z)). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. rewrite <- Qplus_0_l at 1. apply Qplus_le_l. apply Qpos_nonneg. - apply (CRle_trans (CR_b_upperBound_2 y z)). apply CRle_Qle. apply (Qle_trans _ ((1#1)*proj1_sig (CR_b (1#1) y + (1#1))%Qpos * proj1_sig ((CR_b (1#1) z) + (1#1))%Qpos)). rewrite Qmult_1_l. apply (Qpos_mult_le_compat (CR_b (1#1) y) (CR_b (1#1) z)). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. rewrite <- Qplus_0_l at 1. apply Qplus_le_l. apply Qpos_nonneg. - apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) y))%Q)). 2: apply CR_b_lowerBound. apply CRle_Qle. apply Qopp_le_compat. apply (Qle_trans _ (` (CR_b (1#1)%Qpos y) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_yfactor_le. - apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) y))%Q)). apply CR_b_upperBound. apply CRle_Qle. apply (Qle_trans _ (` (CR_b (1#1)%Qpos y) + (1#1))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. discriminate. apply CRmult_assoc_yfactor_le. 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