proposition: Lemma everyOther_nbz : forall (s : Stream Q) (e : QposInf), (NearBy 0 e s) -> NearBy 0 e (everyOther s).
proof: Proof. cofix everyOther_nbz. intros [s [b r]] x [H [_ Hs]]. constructor;[|apply everyOther_nbz];assumption. 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