proposition: Lemma Stream_Bound_nbz : forall a b e, (StreamBounds a b) -> NearBy 0 e a -> NearBy 0 e b.
proof: Proof. cofix Stream_Bound_nbz. intros a b e Hb Ha. constructor. destruct Hb as [[Hb1 Hb2] _]. destruct e as [e|];[|constructor]. destruct Ha as [[Ha1 Ha2] _]. simpl in *. split. apply Qle_trans with (-(CoqStreams.hd a -0)). apply Qopp_le_compat. assumption. ring_simplify. assumption. apply Qle_trans with (CoqStreams.hd a - 0). ring_simplify. assumption. assumption. eapply Stream_Bound_nbz. destruct Hb as [_ Hb]. change (StreamBounds (CoqStreams.tl a) (CoqStreams.tl b)) in Hb. apply Hb. destruct Ha as [_ Ha]. 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