proposition: Lemma CompactCompleteSubset : forall x, CompleteSubset _ (fun z => inCompact z x).
proof: Proof. intros x a H. pose (exist (Qlt 0) (1#2) eq_refl) as half. exists (Cjoin a). abstract ( intros e1 e2; unfold inCompact in H; eapply FinSubset_ball_weak_le; [|apply (H (half*e1) (half*e1) e2)%Qpos]; simpl; rewrite -> Qle_minus_iff; ring_simplify; auto with *; apply Qmult_le_0_compat; auto with * ). apply CunitCjoin. Defined.
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