proposition: Lemma iterate_add : forall (p q:positive) (x : X), iterate (p+q)%positive x ≡ iterate p (iterate q x).
proof: Proof. apply (Pos.peano_ind (fun p => forall (q : positive) (x : X), iterate (p + q) x ≡ iterate p (iterate q x))). - intros. rewrite Pos.add_1_l, iterate_succ. reflexivity. - intros. rewrite iterate_succ. rewrite <- Pos.add_1_l, <- Pos.add_assoc, Pos.add_1_l. rewrite iterate_succ, H. 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