proposition: Lemma InCompact_approx : forall (Y : Compact X) (x : Complete X) (d:Qpos) (e:Q), inCompact x Y -> proj1_sig d < e -> {y:X | In y (approximate Y d) /\ ball e x (Cunit y)}.
proof: Proof. intros. unfold inCompact in H. assert (0 < (1#4) * (e - proj1_sig d)). { apply Qlt_minus_iff in H0. apply (Qpos_ispos ((1#4)*exist _ _ H0)). } specialize (H (exist _ _ H1) d). simpl in H. assert ((1#4) * (e - proj1_sig d) + proj1_sig d < (1#2) * (proj1_sig d + e)). { apply (Qplus_lt_l _ _ (-(1#4)*e - (1#2)*proj1_sig d)). ring_simplify. apply Qmult_lt_l. reflexivity. exact H0. } pose proof (AlmostInExists_weak H2 H) as [y [H3 H4]]. exists y. split. exact H3. intros d1 d2. simpl. apply (@ball_weak_le _ (proj1_sig d1 + ((1 # 4) * (e - proj1_sig d)) + (1 # 2) * (proj1_sig d + e))). rewrite <- Qplus_assoc, <- Qplus_assoc. apply Qplus_le_r. apply (Qle_trans _ (e + 0)). rewrite Qplus_0_r. apply (Qplus_le_r _ _ (-(3#4)*e)). ring_simplify. setoid_replace (2#8) with (1#4) by reflexivity. apply Qmult_le_l. reflexivity. apply Qlt_le_weak, H0. apply Qplus_le_r, Qpos_nonneg. apply ball_triangle with (b:=(approximate x (Qpos2QposInf (exist _ _ H1)))). - apply (regFun_prf x d1 (exist _ _ H1)). - exact H4. 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