proposition: Lemma CompactTotallyBoundedB : forall s e x, (inCompact x s) -> exists y, In y (CompactTotalBound s e) /\ ball (proj1_sig e) x y.
proof: Proof. intros s e x Hx. assert (Z:proj1_sig ((1 # 20) * e + (1 # 5) * e)%Qpos < proj1_sig ((7 # 20) * e)%Qpos). rewrite -> Qlt_minus_iff. simpl. ring_simplify. apply (Qpos_ispos ((200#2000)*e)). destruct (AlmostInExists_weak Z (Hx _ _)) as [y [Hy0 Hy1]]. clear Z. unfold CompactTotalBound. revert Hy0. cut (forall pt Hpt, ball ((3#5)*proj1_sig e) (Cunit pt) (@CompactTotallyBounded_fun s (1#4)%Qpos ((1#5)*e) ((1#5)*e) QuarterLeHalf pt Hpt)). { generalize (CompactTotallyBounded_fun s (1#4)%Qpos ((1#5)*e) ((1#5)*e) QuarterLeHalf). generalize (approximate s ((1 # 5) * e)%Qpos). intros l. induction l. contradiction. intros F HF [H|H]. econstructor. split. left. reflexivity. rewrite <- H in Hy1. clear - Hy1 HF. assert (QposEq e ((1#20)*e + (7#20)*e + (3#5)*e)) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. apply ball_triangle with (Cunit a);[|apply HF]. apply ball_triangle with (Cunit (approximate x ((1#20)*e)%Qpos)). apply ball_approx_r. rewrite -> ball_Cunit. assumption. edestruct (fun F HF => IHl F HF H) as [y' [Hy'0 Hy'1]]; [|exists y';split;[right;apply Hy'0|assumption]]. intros pt Hpt. apply HF. } intros pt Hpt. assert (QposEq ((3#5)*e) ((5#3)*((1#5)*e) + (4#3)*((1#5)*e))) by (unfold QposEq; simpl; ring). unfold QposEq in H. rewrite H. clear H. pose proof (CompactTotallyBoundedNotFar s (1#4)%Qpos ((1 # 5) * e) ((1 # 5) * e) QuarterLeHalf Hpt). setoid_replace (proj1_sig ((5 # 3) * ((1 # 5) * e) + (4 # 3) * ((1 # 5) * e))%Qpos) with (((1 + proj1_sig (1 # 4)%Qpos) * proj1_sig ((1 # 5) * e)%Qpos + proj1_sig ((1 # 5) * e)%Qpos) / (1 - proj1_sig (1 # 4)%Qpos)). apply H. simpl. unfold Qdiv. setoid_replace (/ (1 - (1 # 4))) with (4#3) by reflexivity. ring. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround