proposition: Lemma closeRationalL : forall (a b t d : IR) (Hab : a [<=] b), Compact Hab t -> a[<]t -> [0][<]d -> {q : Q | Compact Hab q /\ AbsIR (t[-]q)[<=]d}.
proof: Proof. intros ? ? ? ? ? p Hcc Hdp. pose proof (Max_less _ _ _ (ltMinusRhs _ 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 (inj_Q IR q[<=] b) as Hqb by (eauto using less_leEq, less_leEq_trans). assert (a[<=] inj_Q IR q) as Haq by (eauto using less_leEq, less_leEq_trans, leEq_less_trans, rht_leEq_Max). split;[exact (Haq,Hqb)|]. rewrite AbsIR_eq_x;[|eauto 4 using shift_zero_leEq_minus, less_leEq]. apply shift_minus_leEq. apply shift_leEq_plus'. unfold Q2R. pose proof (lft_leEq_Max (t[-]d) a). apply less_leEq. eapply leEq_less_trans; eauto. Qed.
imports: CoRN.ftc.FTC Coq.setoid_ring.Ring CoRN.tactics.CornTac CoRN.algebra.CRing_as_Ring CoRN.ftc.Derivative CoRN.ftc.Integral