proposition: Lemma CRlt_trans (x y z: CR): x < y -> y < z -> x < z.
proof: Proof. intros [q H] [r H0]. exists (q+r)%Qpos. rewrite <- (doubleSpeed_Eq z). rewrite <- (doubleSpeed_Eq x). intro e. simpl. unfold Cap_raw; simpl. unfold Cap_raw; simpl. specialize (H ((1#2)*e)%Qpos). simpl in H. specialize (H0 ((1#2)*e)%Qpos). simpl in H0. unfold Cap_raw in H0; simpl in H0. unfold Cap_raw in H0; simpl in H0. unfold Cap_raw in H; simpl in H. unfold Cap_raw in H; simpl in H. apply (Qplus_le_compat _ _ _ _ H) in H0. setoid_replace (- ((1 # 2) * ` e) + - ((1 # 2) * ` e))%Q with (-`e)%Q in H0 by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ H0). ring_simplify. apply Qle_refl. 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