proposition: Lemma CRlt_Qmid (x y: CR): x < y -> sigT (λ q: Q, prod (x < 'q) ('q < y)).
proof: Proof. Proof with auto. intros [q E]. set (quarter := ((1#4)*q)%Qpos). exists (proj1_sig quarter + (approximate x quarter + proj1_sig quarter))%Q. split. apply CRle_lt_trans with (' (0 + (approximate x quarter + proj1_sig quarter))%Q)%CR... rewrite Qplus_0_l... apply CRlt_Qlt. apply Qplus_lt_l... apply CRlt_le_trans with (x + 'proj1_sig q)%CR. apply CRlt_le_trans with (' (approximate x quarter - proj1_sig quarter + proj1_sig q)%Q)%CR. apply CRlt_Qlt. setoid_replace (proj1_sig q) with (proj1_sig quarter + proj1_sig quarter + proj1_sig quarter + proj1_sig quarter)%Q. ring_simplify. apply Qplus_lt_l. apply Qmult_lt_compat_r... reflexivity. simpl. unfold equiv, stdlib_rationals.Q_eq; ring. rewrite <- CRplus_Qplus. apply CRplus_le_compat... apply CRle_refl. apply CRplus_le_r with (-x)%CR. CRring_replace (x + 'proj1_sig q - x) ('proj1_sig q)... 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