proposition: Lemma Str_alt_decr_tl : forall x p, Str_alt_decr x -> Str_alt_decr (CRstreams.iterate _ f p x).
proof: Proof. assert (forall x, Str_alt_decr x -> Str_alt_decr (f x)). { intros x H p. specialize (H (Pos.succ p)). unfold Str_pth. unfold Str_pth in H. rewrite <- iterate_shift, <- iterate_succ. rewrite <- iterate_shift, <- iterate_succ. apply H. } intros x p. revert p x. apply (Pos.peano_ind (fun p => forall (x : X * Q), Str_alt_decr x → Str_alt_decr (CRstreams.iterate (X * Q) f p x))). - intros. simpl. apply H, H0. - intros. rewrite iterate_succ. apply H, H0, H1. 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