proposition: Lemma iterate_succ : forall (p:positive) (x : X), iterate (Pos.succ p) x ≡ f (iterate p x).
proof: Proof. induction p. - intro x. simpl. rewrite IHp. f_equal. rewrite IHp. f_equal. rewrite iterate_shift. reflexivity. - intro x. simpl. rewrite iterate_shift, iterate_shift. reflexivity. - 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