proposition: Lemma CRstream_opp_limit_zero : forall (X:Type) (f : X*Q->X*Q) x cvmod, Limit_zero X f x cvmod -> Limit_zero X (CRstreams.CRstream_opp X f) (let (y, r) := x in (y, - r)) cvmod.
proof: Proof. intros. intro e. specialize (H e). pose proof (CRstreams.CRstream_opp_pth X f x (cvmod e)). unfold Str_pth. unfold Str_pth in H. destruct (CRstreams.iterate (X * Q) f (cvmod e) x) as [y r]. destruct x as [x q]. unfold negate, Q_opp. destruct (CRstreams.iterate (X * Q) (CRstream_opp X f) (cvmod e) (x, (- q)%Q)). unfold snd. unfold snd in H. destruct H0. subst q0. rewrite Qabs_opp. exact H. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra