proposition: Lemma CRlt_linear : forall x y z : CR, x < z -> (sum (x < y) (y < z)).
proof: Proof. intros. destruct (CRlt_Qmid _ _ H) as [q [H0 H1]]. destruct (CRlt_Qmid _ _ H1) as [r [H2 H3]]. assert (Qlt 0 ((1#2)*(r-q))) as qltr. { rewrite <- (Qmult_0_r (1#2)). apply Qmult_lt_l. reflexivity. unfold Qminus. rewrite <- Qlt_minus_iff. apply Qlt_from_CRlt, H2. } destruct (Qlt_le_dec (approximate y (Qpos2QposInf (exist (Qlt 0) _ qltr))) ((1#2)*(q+r))). - right. refine (CRle_lt_trans _ ('r) _ _ H3). pose proof (upper_CRapproximation y (exist (Qlt 0) _ qltr)). apply (@CRle_trans _ _ _ H4). apply CRle_Qle. apply (Qle_trans _ ((1 # 2) * (q + r) + (1 # 2) * (r - q))). apply Qplus_le_l, Qlt_le_weak, q0. ring_simplify. apply Qle_refl. - left. apply (CRlt_le_trans _ ('q) _ H0). pose proof (lower_CRapproximation y (exist (Qlt 0) _ qltr)). refine (@CRle_trans _ _ _ _ H4). apply CRle_Qle. apply (Qle_trans _ ((1 # 2) * (q + r) - (1 # 2) * (r - q))). ring_simplify. apply Qle_refl. apply Qplus_le_l, q0. 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