proposition: Lemma UniformPartition_fine : forall (n:positive) (x:Q), l <= x <= r -> {y | In y (UniformPartition n) /\ Qabs (x - y) <= ((r-l)/((2#1)*inject_Z (Zpos n)))}.
proof: Proof. intros n x Hx. destruct (Qlt_le_dec_fast x r). - exists (f n (rasterize1 n x)). abstract ( destruct Hx as [Hlx Hxr]; split; [apply in_map; rewrite -> UniformPartitionZ; split; [apply rasterize1_boundL; auto |apply rasterize1_boundR; auto] |apply rasterize1_close; apply Qle_lt_trans with x; auto]). - exists (f n (Zpos n - 1)). apply UniformPartition_fine_aux; assumption. Defined.
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