proposition: Lemma StreamInCompactApprox : forall n s k d1 d2 pt Hpt, {q:Qpos | InFinEnumC (@CompactImproveApproximation s k d1 d2 pt Hpt n) (approximate s q) & QposEq q (Qpos_power k (Z.of_nat n)*d1) }.
proof: Proof. induction n. intros. exists d1. assumption. unfold QposEq; simpl; ring. intros. unfold Str_nth. simpl. destruct (@HausdorffBallHausdorffBallStrong X locatedX (@proj1_sig Q (Qlt 0) d1 + @proj1_sig Q (Qlt 0) k * @proj1_sig Q (Qlt 0) d1) (@approximate _ (FinEnum_ball X) s d1) (@approximate _ (FinEnum_ball X) s (k * d1)%Qpos) (@regFun_prf _ (FinEnum_ball X) s d1 (k * d1)%Qpos)) as [f _]. destruct (f pt Hpt d2) as [pt' [Hpt' _]]. destruct (IHn s k (k*d1) (k*d2) pt' Hpt')%Qpos as [q Hq Hq0]. exists q. apply Hq. rewrite Zpos_P_of_succ_nat. unfold Z.succ. unfold QposEq, Qpos_power, proj1_sig. simpl. rewrite Z.add_comm. rewrite -> Qpower_plus. simpl. unfold QposEq, proj1_sig in Hq0. simpl in Hq0. rewrite Hq0. unfold proj1_sig. ring. destruct k. simpl. intro abs. apply (Qlt_not_le _ _ q0). rewrite abs. 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