proposition: Lemma CRplus_assoc (x y z: CR): x + (y + z) == (x + y) + z.
proof: Proof. intros. intros e1 e2. destruct x,y,z; simpl; unfold Cap_raw; simpl. unfold Cap_raw; simpl. apply AbsSmall_Qabs. setoid_replace (approximate ((1 # 2) * e1)%Qpos + (approximate0 ((1 # 2) * ((1 # 2) * e1))%Qpos + approximate1 ((1 # 2) * ((1 # 2) * e1))%Qpos) - (approximate ((1 # 2) * ((1 # 2) * e2))%Qpos + approximate0 ((1 # 2) * ((1 # 2) * e2))%Qpos + approximate1 ((1 # 2) * e2)%Qpos))%Q with ((approximate ((1 # 2) * e1)%Qpos - approximate ((1 # 2) * ((1 # 2) * e2))%Qpos) + (approximate0 ((1 # 2) * ((1 # 2) * e1))%Qpos - approximate0 ((1 # 2) * ((1 # 2) * e2))%Qpos) + (approximate1 ((1 # 2) * ((1 # 2) * e1))%Qpos - approximate1 ((1 # 2) * e2)%Qpos))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). rewrite Qplus_0_r. setoid_replace (` e1 + ` e2)%Q with (((1#2)* ` e1 + (1#2)*((1#2) * `e2)) + ((1#2)*((1#2)* `e1) + (1#2)*((1#2)*`e2)) + ((1#2)*((1#2)* `e1) + (1#2)* ` e2))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qabs_triangle _ _)). apply Qplus_le_compat. - apply AbsSmall_Qabs. apply (regFun_prf ((1#2)*e1)%Qpos ((1#2)*((1#2)*e2))%Qpos). - apply AbsSmall_Qabs. apply (regFun_prf0 ((1#2)*((1#2)*e1))%Qpos ((1#2)*((1#2)*e2))%Qpos). - apply AbsSmall_Qabs. apply (regFun_prf1 ((1#2)*((1#2)*e1))%Qpos ((1#2)*e2)%Qpos). 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