proposition: Lemma CRstream_opp_pth : forall (X:Type) (f : X*Q->X*Q) (xq : X*Q) (p : positive), let (y,r) := iterate _ f p xq in let (z,s) := iterate _ (CRstream_opp X f) p (let (x,q):=xq in (x,-q)) in y ≡ z /\ s ≡ -r.
proof: Proof. intros X f xq. apply Pos.peano_ind. - simpl. destruct xq as [x q]. unfold CRstream_opp. replace (--q) with q. destruct (f (x,q)). split; reflexivity. destruct q. unfold Qopp; simpl. rewrite Z.opp_involutive. reflexivity. - intros IHp H. rewrite CRstreams.iterate_succ, CRstreams.iterate_succ. destruct (iterate _ f IHp xq), (iterate _ (CRstream_opp X f) IHp (let (x0, q0) := xq in (x0, - q0))). unfold CRstream_opp. destruct H. subst q0. subst x0. replace (--q) with q. destruct (f (x,q)). split; reflexivity. destruct q. unfold Qopp; simpl. rewrite Z.opp_involutive. reflexivity. 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