proposition: Lemma SumStream_wd : forall (p:positive) (X Y:Type) (f : X*Q -> X*Q) (g : Y*Q -> Y*Q) (x : X*Q) (y : Y*Q), (forall p:positive, Str_pth _ f p x == Str_pth _ g p y) -> snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (x,0)) == snd (CRstreams.iterate _ (fun y : Y * Q * Q => let (z0, r1) := g (fst y) in (z0, r1, r1 + snd y)) p (y,0)).
proof: Proof. apply (Pos.peano_ind (fun p => forall (X Y:Type) (f : X*Q -> X*Q) (g : Y*Q -> Y*Q) (x : X*Q) (y : Y*Q), (forall p:positive, Str_pth _ f p x == Str_pth _ g p y) -> snd (CRstreams.iterate _ (fun y : X * Q * Q => let (z0, r1) := f (fst y) in (z0, r1, r1 + snd y)) p (x,0)) == snd (CRstreams.iterate _ (fun y : Y * Q * Q => let (z0, r1) := g (fst y) in (z0, r1, r1 + snd y)) p (y,0)))). - intros. simpl. specialize (H xH). unfold Str_pth in H. simpl in H. destruct (f x), (g y). simpl. simpl in H. rewrite H. reflexivity. - intros. pose proof (H0 (Pos.succ p)). unfold Str_pth in H1. rewrite iterate_succ, iterate_succ in H1. rewrite iterate_succ, iterate_succ, SumStream_fst, SumStream_fst. unfold fst. destruct (f (CRstreams.iterate (X * Q) f p x)). unfold snd at 1. destruct (g (CRstreams.iterate (Y * Q) g p y)). unfold snd at 3. specialize (H X Y f g x y H0). rewrite H. simpl in H1. rewrite H1. reflexivity. 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