proposition: Lemma InCompact_approxC : forall (Y : Compact X) (x : Complete X) (d:Qpos), inCompact x Y -> ~~exists y:X, In y (approximate Y d) /\ ball (proj1_sig d) x (Cunit y).
proof: Proof. intros. intro abs. apply (infinitePidgeonHolePrinicple _ (approximate Y d) (fun n y => ball (proj1_sig d+(1#Pos.of_nat n)) x (Cunit y))). - intros n. apply existsWeaken. destruct (@InCompact_approx Y x d (proj1_sig d + (1 # Pos.of_nat n)) H) as [t [H0 H1]]. apply (Qle_lt_trans _ (proj1_sig d+0)). rewrite Qplus_0_r. apply Qle_refl. apply Qplus_lt_r. reflexivity. exists t. split. intro H3; contradiction. exact H1. - intros t [H0 H1]. contradict abs. exists t. split. exact H0. apply ball_closed. intros e epos. destruct e as [a n]. specialize (H1 (Pos.to_nat n)). apply (msp_stable (msp (Complete X))). intro abs. unfold existsC in H1. contradict H1; intros k [H1 H3]. contradict abs. apply (ball_weak_le) with (e:=proj1_sig d + (1 # Pos.of_nat k)). apply Qplus_le_r. apply (Qle_trans _ (1#n)). unfold Qle; simpl. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H1. apply (Nat.lt_le_trans _ _ _ (Pos2Nat.is_pos n)) in H1. destruct k. inversion H1. discriminate. unfold Qle; simpl. apply (Z.mul_le_mono_nonneg_r 1 a (Z.pos n)). discriminate. unfold Qlt in epos. simpl in epos. rewrite Z.mul_1_r in epos. apply (Zlt_le_succ 0 a), epos. exact H3. 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