proposition: Lemma CompactTotallyBoundedStreamCauchyLemma : forall n (k d:Qpos), proj1_sig k < 1 -> 0 < (proj1_sig d*(1-proj1_sig k^Z.of_nat (S n))/(1-proj1_sig k)).
proof: Proof. intros n k d Hk. unfold Qdiv. rewrite <- Qmult_assoc. apply (Qle_lt_trans _ (proj1_sig d * 0)). rewrite Qmult_0_r. apply Qle_refl. apply Qmult_lt_l. apply Qpos_ispos. apply (Qle_lt_trans _ ((1 - proj1_sig k ^ Z.of_nat (S n)) * 0)). rewrite Qmult_0_r. apply Qle_refl. apply Qmult_lt_l. unfold Qminus. rewrite <- Qlt_minus_iff. induction n. assumption. simpl. rewrite Pplus_one_succ_l. rewrite -> Qpower_plus_positive. apply Qlt_trans with (proj1_sig k*1). apply Qmult_lt_l. apply Qpos_ispos. exact IHn. rewrite Qmult_1_r. exact Hk. apply Qlt_shift_inv_l. unfold Qminus. rewrite <- Qlt_minus_iff. assumption. ring_simplify. constructor. 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