proposition: Lemma UniformPartition_inside : forall n x, In x (UniformPartition n) -> l <= x <= r.
proof: Proof. intros n x. unfold UniformPartition. assert (forall z, In z (iterateN_succ 0%Z n) -> (0 <= z < Zpos n)%Z) as H. { intros. apply UniformPartitionZ in H. exact H. } revert H. generalize (iterateN_succ 0%Z n). intros s Hs H. induction s. contradiction. destruct H as [H | H];auto with *. rewrite <- H. destruct (Hs a) as [Hz0 Hz1]; auto with *. clear - Hz0 Hz1 Hlr. split. unfold f, Qdiv. rewrite <- (Qplus_0_r l) at 1. apply Qplus_le_r. apply Qle_shift_div_l. reflexivity. rewrite Qmult_0_l. apply Qmult_le_0_compat. unfold Qminus. rewrite <- Qle_minus_iff. exact Hlr. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. apply (Z.le_trans _ (1*a+0)%Z). rewrite Z.add_0_r, Z.mul_1_l. exact Hz0. apply Z.add_le_mono. apply Z.mul_le_mono_nonneg_r. exact Hz0. discriminate. discriminate. unfold f. apply (Qplus_le_r _ _ (-l)). rewrite Qplus_assoc. rewrite (Qplus_comm (-l)), Qplus_opp_r, Qplus_0_l. apply Qle_shift_div_r. reflexivity. rewrite (Qplus_comm (-l)), Qmult_comm, (Qmult_comm (r+-l)). apply Qmult_le_compat_r. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. rewrite Z.add_comm, Z.add_1_l. apply Zlt_le_succ. apply Z.mul_lt_mono_pos_l. reflexivity. exact Hz1. rewrite <- Qle_minus_iff. exact Hlr. 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