proposition: Lemma CRstream_opp_decr : forall (X:Type) (f : X*Q->X*Q) x, Str_alt_decr X f x -> Str_alt_decr X (CRstreams.CRstream_opp X f) (let (y, r) := x in (y, - r)).
proof: Proof. intros X f x H p. specialize (H p). pose proof (CRstreams.CRstream_opp_pth X f x p). pose proof (CRstreams.CRstream_opp_pth X f x (Pos.succ p)). unfold Str_pth. unfold Str_pth in H. destruct x as [x q]. unfold negate, Q_opp. destruct (CRstreams.iterate _ f p (x,q)). destruct (CRstreams.iterate _ f (Pos.succ p) (x,q)). unfold snd in H. destruct (CRstreams.iterate _ (CRstreams.CRstream_opp X f) (Pos.succ p) (x, (-q)%Q)). destruct (CRstreams.iterate _ (CRstreams.CRstream_opp X f) p (x, (-q)%Q)). unfold snd. destruct H1. subst q2. subst x2. destruct H0. subst q3. subst x3. destruct H. split. - rewrite Qabs_opp, Qabs_opp. exact H. - setoid_replace (- q1 * - q0)%Q with (q1*q0)%Q. exact H0. unfold equiv, Q_eq. ring. 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