proposition: Lemma qi_lim_zero : forall q : IR, [0] [<=] q -> q [<] [1] -> SeqLimit (fun i => q[^]i) [0].
proof: Proof. intros q H H0. unfold SeqLimit in |- *. unfold AbsSmall in |- *. intros. elim (qi_yields_zero q H H0 e); auto. intro N. intros. exists (S N). intros. split. apply less_leEq. apply less_leEq_trans with ZeroR. astepr ( [--]ZeroR). apply inv_resp_less. auto. astepr (q[^]m). apply nexp_resp_nonneg. auto. astepl (q[^]m). replace m with (N + (m - N)). astepl (q[^]N[*]q[^] (m - N)). astepr (e[*][1]). apply mult_resp_leEq_both. apply nexp_resp_nonneg. auto. apply nexp_resp_nonneg. auto. auto. astepr (OneR[^] (m - N)). apply nexp_resp_leEq. auto. apply less_leEq. auto. auto with arith. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero