proposition: Lemma iterateN_succ_length : forall n z, length (iterateN_succ z n) = Pos.to_nat n.
proof: Proof. induction n. - intro z. simpl. rewrite Pos2Nat.inj_xI. apply f_equal. rewrite app_length, IHn, IHn. simpl. rewrite Nat.add_0_r. reflexivity. - intro z. simpl. rewrite app_length, IHn, IHn. rewrite Pos2Nat.inj_xO. simpl. rewrite Nat.add_0_r. reflexivity. - reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact CoRN.metric2.LocatedSubset CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.metric2.Qmetric Coq.QArith.Qround Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Classic