proposition: Lemma UniformPartitionZ : forall n a z, In z (iterateN_succ a n) <-> (a <= z < a + Zpos n)%Z.
proof: Proof. split. - intro H. apply (In_nth _ _ 0%Z) in H. destruct H as [p [H H0]]. subst z. rewrite iterateN_succ_length in H. rewrite iterateN_succ_nth. 2: exact H. split. rewrite <- (Z.add_0_r a) at 1. apply Z.add_le_mono_l. apply Nat2Z.is_nonneg. apply Z.add_lt_mono_l. destruct p. reflexivity. rewrite <- (Nat2Pos.id (S p)) in H. 2: discriminate. apply Pos2Nat.inj_lt in H. simpl. rewrite Pos.of_nat_succ. exact H. - revert n z a. induction n; intros. + simpl. destruct (Z.le_gt_cases z a). left. apply Z.le_antisymm. apply H. exact H0. right. destruct (Z.le_gt_cases (Z.succ a + Z.pos n) z). apply in_app_iff. right. apply IHn. split. apply H1. rewrite <- Z.add_assoc, Z.add_diag. apply (Z.lt_le_trans _ _ _ (proj2 H)). rewrite <- Z.add_1_l, (Z.add_comm 1). rewrite <- Z.add_assoc. apply Z.le_refl. apply in_app_iff. left. apply IHn. split. apply Zlt_le_succ, H0. exact H1. + simpl. destruct (Z.le_gt_cases (a + Z.pos n) z). apply in_app_iff. right. apply IHn. split. apply H0. rewrite <- Z.add_assoc, Z.add_diag. apply H. apply in_app_iff. left. apply IHn. split. apply H. exact H0. + left. destruct H. apply Z.le_antisymm. exact H. rewrite Z.add_comm, Z.add_1_l in H0. apply Zlt_succ_le, H0. 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