proposition: Lemma CompactTotallyBoundedNotFar : forall (s:Compact X) (k d1 d2:Qpos) (khalf : proj1_sig k <= 1#2) (pt:X) (Hpt : InFinEnumC pt (approximate s d1)), ball (((1 + proj1_sig k)*proj1_sig d1 + proj1_sig d2) / (1 - proj1_sig k)) (Cunit pt) (@CompactTotallyBounded_fun s k d1 d2 khalf pt Hpt).
proof: Proof. intros s k d1 d2 khalf pt Hpt e1 e2. simpl. assert (proj1_sig k < 1) as Z. { apply (Qle_lt_trans _ _ _ khalf). reflexivity. } pose proof (CompactTotallyBoundedStreamCauchyLemma (Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2)) _ (((1#1)+k)*d1 + d2)%Qpos Z) as Z0. apply ball_weak_le with (proj1_sig (exist _ _ Z0)). 2: apply CompactImproveApproxCauchy1; exact Z. simpl. apply Qle_trans with (((1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2) / (1 - proj1_sig k)). apply Qmult_le_compat_r. - rewrite <- (Qmult_1_r ( (1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2)) at 2. apply Qmult_le_l. apply (Qpos_ispos (((1#1)+k)*d1 + d2)). rewrite -> Qle_minus_iff. ring_simplify. apply Qpower_pos_positive. apply Qpos_nonneg. - apply Qlt_le_weak, Qinv_lt_0_compat. unfold Qminus. rewrite <- Qlt_minus_iff. exact Z. - apply (Qle_trans _ (0 + (((1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2) / (1 - proj1_sig k)) + 0)). rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. apply Qplus_le_compat. 2: apply Qpos_nonneg. apply Qplus_le_compat. apply Qpos_nonneg. apply Qle_refl. 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