proposition: Lemma mult_Streams_nbz : forall {s1 s2 : Stream Q} {x : QposInf}, (NearBy 0 x s1) -> forall {y : QposInf}, NearBy 0 y s2 -> NearBy 0 (x*y) (mult_Streams s1 s2).
proof: Proof. unfold NearBy. cofix mult_Streams_nbz. intros s1 s2 x [Ha0 Hs1] y [Hb0 Hs2]. constructor. 2: apply (mult_Streams_nbz (CoqStreams.tl s1) (CoqStreams.tl s2)); assumption. destruct x as [x|];[|constructor]. destruct y as [y|];[|constructor]. simpl. unfold Qball. unfold QAbsSmall. setoid_replace ((CoqStreams.hd s1 * CoqStreams.hd s2)%mc - 0)%Q with ((CoqStreams.hd s1 - 0) * (CoqStreams.hd s2 - 0)). apply Qmult_AbsSmall; assumption. ring_simplify. reflexivity. Qed.
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