proposition: Lemma Stream_Bound_zl : forall a b, (StreamBounds a b) -> Limit a 0 -> Limit b 0.
proof: Proof. intros a b H Ha e. assert (Ha':=(Ha e)); clear Ha. generalize b H; clear b H. induction Ha'; intros b Hb. left. apply Stream_Bound_nbz with x; assumption. right. rename H0 into IHHa'. intros _. apply (IHHa' tt). 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