proposition: Lemma mult_Streams_zl : forall (a b : Stream Q), (Limit a 0) -> forall (x:Qpos), NearBy 0 x b -> Limit (mult_Streams a b) 0.
proof: Proof. intros a b Ha x Hb e. assert (H:=Ha (e * (Qpos_inv x))%QposInf). generalize b Hb. clear b Hb. induction H; intros b Hb. left. abstract ( destruct e as [e|];[|apply ForAll_True]; assert (Heq:proj1_sig e== proj1_sig ((e*Qpos_inv x)*x)%Qpos);[ simpl; field; apply Qpos_nonzero |rewrite -> (NearBy_comp _ _ (ball_refl _ 0 (Qle_refl 0)) _ _ Heq ); apply (mult_Streams_nbz H Hb)] ). right. simpl. rename H0 into IHExists. intros. apply (IHExists tt). apply Limit_tl; assumption. destruct Hb; assumption. Defined.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams