proposition: Lemma closeRationalR : forall (a b t d : IR) (Hab : a [<=] b), Compact Hab t -> t[<]b -> [0][<]d -> {q : Q | Compact Hab q /\ AbsIR (t[-]q)[<=]d}.
proof: Proof. intros ? ? ? ? ? p Hcc Hdp. pose proof (less_Min _ _ _ (ltAddRhs t d Hdp) Hcc) as Hmlt. pose proof (Q_dense_in_CReals' _ _ _ Hmlt) as Hqr. destruct Hqr as [q Hqr Hql]. exists q. simpl in p. unfold Q2R in p. destruct p as [pl pr]. assert ( a[<=]inj_Q IR q) as Haq by (eauto using less_leEq, leEq_less_trans). assert (inj_Q IR q[<=] b) as Hqb by (eauto using less_leEq, less_leEq_trans, Min_leEq_rht). split;[exact (Haq,Hqb)|]. rewrite AbsIR_minus. unfold Q2R. rewrite AbsIR_eq_x;[|eauto 4 using shift_zero_leEq_minus, less_leEq]. apply shift_minus_leEq. rewrite cag_commutes_unfolded. eauto using less_leEq,leEq_less_trans,leEq_reflexive, less_leEq_trans,Min_leEq_lft. Defined.
imports: CoRN.ftc.FTC Coq.setoid_ring.Ring CoRN.tactics.CornTac CoRN.algebra.CRing_as_Ring CoRN.ftc.Derivative CoRN.ftc.Integral