proposition: Lemma iterateN_succ_nth : forall n (j:nat) s z, (j < Pos.to_nat n)%nat -> nth j (iterateN_succ s n) z = (s + Z.of_nat j)%Z.
proof: Proof. induction n. - intros. simpl. destruct j. simpl. rewrite Z.add_0_r. reflexivity. destruct (le_lt_dec (Pos.to_nat n) j) as [l0|l0]. + rewrite <- (iterateN_succ_length n (Z.succ s)) in l0. rewrite (app_nth2 _ _ z l0). pose proof (Nat.le_exists_sub _ _ l0) as [k [H0 _]]. subst j. rewrite Nat.add_sub. rewrite IHn. rewrite iterateN_succ_length. rewrite Nat2Z.inj_succ, Nat2Z.inj_add, <- positive_nat_Z. ring. rewrite (iterateN_succ_length n (Z.succ s)), Pos2Nat.inj_xI in H. simpl in H. rewrite Nat.add_0_r in H. apply le_S_n in H. apply (Nat.add_le_mono_r _ _ (Pos.to_nat n)). exact H. + rewrite <- (iterateN_succ_length n (Z.succ s)) in l0. rewrite (app_nth1 _ _ z l0). rewrite IHn. rewrite Nat2Z.inj_succ. ring. rewrite <- (iterateN_succ_length n (Z.succ s)). exact l0. - intros. simpl. destruct (le_lt_dec (Pos.to_nat n) j) as [l0|l0]. + rewrite <- (iterateN_succ_length n s) in l0. rewrite (app_nth2 (iterateN_succ s n) (iterateN_succ (s + Z.pos n) n) z l0). pose proof (Nat.le_exists_sub _ _ l0) as [k [H0 _]]. subst j. rewrite Nat.add_sub. rewrite IHn. rewrite (iterateN_succ_length n s). rewrite Nat2Z.inj_add, <- positive_nat_Z. ring. rewrite (iterateN_succ_length n s), Pos2Nat.inj_xO in H. simpl in H. rewrite Nat.add_0_r in H. apply (Nat.add_le_mono_r _ _ (Pos.to_nat n)). exact H. + rewrite <- (iterateN_succ_length n s) in l0. rewrite (app_nth1 (iterateN_succ s n) (iterateN_succ (s + Z.pos n) n) z l0). apply IHn. rewrite <- (iterateN_succ_length n s). exact l0. - intros. simpl. destruct j. simpl. rewrite Z.add_0_r. reflexivity. exfalso. inversion H. inversion H1. 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