proposition: Lemma UniformPartition_fine_aux : forall (n : positive) (x : Q) (Hx : l <= x <= r) (q : r <= x), In (f n (Zpos n - 1)) (UniformPartition n) /\ Qabs (x - f n (Zpos n - 1)) <= (r - l) / ((2#1) * inject_Z (Zpos n)).
proof: Proof. intros. split. - apply in_map; rewrite -> UniformPartitionZ. split. apply Z.le_0_sub, Pos.le_1_l. rewrite Z.add_comm. apply Z.add_lt_mono_l. reflexivity. - destruct Hx as [_ Hx]. setoid_replace x with r by (apply Qle_antisym; assumption). unfold f. replace (2 * (Z.pos n - 1) + 1)%Z with (2 * Z.pos n - 1)%Z by ring. change (2*Zpos n #1) with ((2#1)*inject_Z (Zpos n)). change (2*Zpos n - 1#1) with (inject_Z (2*Zpos n + - 1)). rewrite Q.Zplus_Qplus. rewrite Q.Zmult_Qmult. change (inject_Z 2) with (2#1). change (inject_Z (-1)) with (-1#1). setoid_replace (r - (l + (r - l) * ((2#1) * inject_Z (Zpos n) + (-1#1)) / ((2#1) * (inject_Z (Zpos n))))) with (((r-l) / ((2#1) * (inject_Z (Zpos n))))) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field; auto). rewrite -> Qabs_pos. apply Qle_refl. apply Qle_shift_div_l. reflexivity. rewrite Qmult_0_l; rewrite -> Qle_minus_iff in Hlr; auto. 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