proposition: Lemma CompactIntervalQ_correct1 : forall (x:CR), inCompact x CompactIntervalQ -> ('l <= x /\ x <= 'r).
proof: Proof. intros x Hx. split. unfold CRle. assert (x - 'l == '(-l)%Q + x)%CR. ring. rewrite -> H. clear H. rewrite -> CRplus_translate. intros e. simpl. rewrite -> Qle_minus_iff. setoid_replace (- l + approximate x e + - - proj1_sig e)%Q with (proj1_sig e + - (l - approximate x e))%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. apply Qle_closed. intros e2. assert (L:=Hx e e2). simpl in L. set (a:=Z.to_pos (Qceiling ((r - l) / (inject_Z 2 * proj1_sig e2)))) in *. assert (L0:=UniformPartition_inside a). induction (UniformPartition a). exfalso; exact (FinSubset_ball_nil L). apply FinSubset_ball_orC in L. destruct L as [ G | L | L] using orC_ind. auto with *. rewrite -> Qball_Qabs in L. eapply Qle_trans;[|apply L]. rewrite <- Qabs_opp. eapply Qle_trans;[|apply Qle_Qabs]. rewrite -> Qle_minus_iff. setoid_replace (- (approximate x e - a0) + - (l - approximate x e))%Q with (a0 + - l)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. destruct (L0 a0); auto with *. apply IHl0; auto with *. unfold CRle. rewrite -> CRplus_translate. intros e. simpl. rewrite -> Qle_minus_iff. setoid_replace (r + - approximate x e + - - proj1_sig e)%Q with (proj1_sig e + - (approximate x e - r))%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. apply Qle_closed. intros e2. assert (L:=Hx e e2). simpl in L. set (a:=Z.to_pos (Qceiling ((r - l) / (inject_Z 2 * proj1_sig e2)))) in *. assert (L0:=UniformPartition_inside a). induction (UniformPartition a). exfalso; exact (FinSubset_ball_nil L). apply FinSubset_ball_orC in L. destruct L as [ G | L | L] using orC_ind. auto with *. rewrite -> Qball_Qabs in L. eapply Qle_trans;[|apply L]. eapply Qle_trans;[|apply Qle_Qabs]. rewrite -> Qle_minus_iff. setoid_replace (approximate x e - a0 + - (approximate x e - r))%Q with (r + - a0)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). rewrite <- Qle_minus_iff. destruct (L0 a0); auto with *. apply IHl0; auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact CoRN.metric2.LocatedSubset CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.metric2.Qmetric Coq.QArith.Qround Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Classic