proposition: Lemma Q_dense_in_compact : forall a b (Hab : a[<=]b) x, a[<]b -> Compact Hab x -> forall e, [0][<]e -> {q:Q | Compact Hab (inj_Q IR q) | AbsSmall e (x[-]inj_Q IR q)}.
proof: Proof. intros a b Hab x Hab0 Hx e He. set (l:=Max a (x[-]e)). set (r:=Min b (x[+]e)). assert (Hlr:l[<]r). destruct Hx as [Hx0 Hx1]. apply less_Min; apply Max_less. assumption. apply shift_minus_less. rstepl (x[+][0]). apply plus_resp_leEq_less; assumption. rstepl (a[+][0]). apply plus_resp_leEq_less; assumption. apply shift_zero_less_minus'. rstepr (e[+]e). apply plus_resp_pos; assumption. destruct (Q_dense_in_CReals' _ _ _ Hlr) as [q Hlq Hqr]. exists q; split. eapply leEq_transitive. apply lft_leEq_Max. apply less_leEq; unfold l in Hlq; apply Hlq. eapply leEq_transitive. apply less_leEq;apply Hqr. apply Min_leEq_lft. apply shift_zero_leEq_minus'. rstepr ((x[+]e)[-]inj_Q IR q). apply shift_zero_leEq_minus. eapply leEq_transitive. apply less_leEq. apply Hqr. apply Min_leEq_rht. apply shift_zero_leEq_minus'. rstepr (inj_Q IR q[-](x[-]e)). apply shift_zero_leEq_minus. eapply leEq_transitive. apply rht_leEq_Max. apply less_leEq. unfold l in Hlq; apply Hlq. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.ftc.MoreIntervals CoRN.reals.fast.CRIR CoRN.tactics.CornTac CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax