proposition: Lemma CompactTotallyBoundedA : forall s e y, In y (CompactTotalBound s e) -> inCompact y s.
proof: Proof. intros s e y. unfold CompactTotalBound. generalize (CompactTotallyBoundedInCompact s (1#4)%Qpos ((1#5)*e) ((1#5)*e) QuarterLeHalf). 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 L [H|H]. rewrite <- H. apply L. eapply (IHl);[|apply H]. intros pt Hpt. apply L. 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