proposition: Lemma CompactIntervalQ_correct2 : forall (x:CR), ('l <= x /\ x <= 'r) -> inCompact x CompactIntervalQ.
proof: Proof. intros x [Hlx Hxr] e1 e2. simpl. set (y:= (Qmax (Qmin (approximate x e1) r) l)). apply (@FinSubset_ball_triangle_l _ (proj1_sig e1) (proj1_sig e2) (approximate x e1) y). - unfold y. apply Qmin_case. apply Qmax_case. auto with *. intros H _. split; simpl. unfold CRle in Hlx. assert (x - 'l == '(-l)%Q + x). ring. rewrite -> H0 in Hlx. clear H0. rewrite -> CRplus_translate in Hlx. assert (H0:=Hlx e1). simpl in H0. clear - H0. unfold Qminus. rewrite Qplus_comm. exact H0. apply Qle_trans with 0%Q; auto with *. clear - H. rewrite Qle_minus_iff in *. setoid_replace (0 + - (approximate x e1 - l))%Q with (l + - approximate x e1)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). exact H. intros H. rewrite -> Qle_max_l in Hlr. simpl. rewrite -> Hlr. split; simpl. clear - H. apply Qle_trans with 0%Q. apply (Qopp_le_compat 0), Qpos_nonneg. rewrite -> Qle_minus_iff in *. rewrite Qplus_0_r. auto. unfold CRle in Hxr. rewrite -> CRplus_translate in Hxr. assert (H0:=Hxr e1). simpl in H0. clear - H0. rewrite -> Qle_minus_iff in *. setoid_replace (proj1_sig e1 + - (approximate x e1 - r))%Q with ( r + - approximate x e1 + - - proj1_sig e1)%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). exact H0. - assert (L: l <= y <= r). { unfold y. auto with *. } set (n:=Z.to_pos (Qceiling ((r - l) / (inject_Z 2 * proj1_sig e2)))). destruct (UniformPartition_fine n L) as [z Hz]. clear - Hz. destruct Hz as [Hz0 Hz1]. induction (UniformPartition n). contradiction. destruct Hz0 as [Hz0 | Hz0]. + intro abs; contradict abs. exists a. split. left. reflexivity. rewrite Hz0. simpl. rewrite -> Qball_Qabs. eapply Qle_trans;[apply Hz1|]. clear Hz1. apply Qle_shift_div_r. reflexivity. unfold Qdiv in n. unfold n. clear n. rewrite (Qmult_comm (r-l)). apply (Qmult_le_l _ _ (/(inject_Z 2 * proj1_sig e2))). apply Qinv_lt_0_compat. apply (Qpos_ispos ((2#1)*e2)). generalize (/ (inject_Z 2 * proj1_sig e2) * (r-l))%Q. intro q. rewrite Qmult_assoc, Qmult_assoc. setoid_replace (/ (inject_Z 2 * proj1_sig e2) * proj1_sig e2 * (2#1))%Q with 1%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). rewrite Qmult_1_l. apply (Qle_trans _ (inject_Z (Qceiling q)) _ (Qle_ceiling _)). rewrite <- Zle_Qle. destruct (Qceiling q). discriminate. apply Z.le_refl. discriminate. apply Qpos_nonzero. + apply FinSubset_ball_cons. apply IHl0, Hz0. 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