proposition: Lemma seq_yields_zero : forall q : IR, [0] [<=] q -> q [<] [1] -> forall c : IR, [0] [<] c -> forall s, (forall i, AbsCC (s i) [<=] q[^]i[*]c) -> CC_SeqLimit s [0].
proof: Proof. intros q zltq qlt1 c zltc s H. unfold CC_SeqLimit in |- *. intros e zlte. generalize (qi_lim_zero q zltq qlt1). intro Hqi. unfold SeqLimit in Hqi. elim (Hqi (e[/] c[//]pos_ap_zero _ c zltc)). intros N HN. exists N. intros m leNm. apply leEq_transitive with (q[^]m[*]c). astepl (AbsCC (s m)). apply H. generalize (HN m leNm). intro H0. unfold AbsSmall in H0. inversion_clear H0. rstepr ((e[/] c[//]pos_ap_zero IR c zltc) [*]c). apply mult_resp_leEq_rht. rstepl (q[^]m[-][0]). assumption. apply less_leEq. assumption. apply shift_less_div. assumption. rstepl ZeroR; assumption. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)