proposition: Lemma data_points_in_range (from: Q) (width: Qpos) (ints: positive) (i : nat) (Ilt: (i < Pos.to_nat ints)%nat): from <= (from + (i * (`width / Zpos ints) + (1 # 2) * (`width / Zpos ints))) <= from + `width.
proof: Proof. Proof with auto with qarith. split. rewrite <- (Qplus_0_r from) at 1. apply Qplus_le_compat... change (0 <= i * ` (width * (1#ints))%Qpos + (1#2) * ` (width * (1#ints))%Qpos)... apply Qplus_le_compat... unfold Qdiv. setoid_replace (i * (`width * / Zpos ints) + (1 # 2) * (`width * / Zpos ints)) with (((i+(1#2)) * / Zpos ints) * `width) by (unfold Q_eq; ring). rewrite <- (Qmult_1_l (`width)) at 2. apply Qmult_le_compat_r... apply Qdiv_le_1. split... apply Qlt_le_weak. rewrite (Zpos_eq_Z_of_nat_o_nat_of_P ints). apply nat_lt_Qlt... Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal CoRN.stdlib_omissions.List Coq.Unicode.Utf8 Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.util.Qsums CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid CoRN.reals.fast.CRArith QnonNeg CoRN.util.Qgcd Coq.Program.Program CoRN.reals.fast.uneven_CRplus CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.tactics.Qauto CoRN.ode.metric CoRN.ode.FromMetric2 MathClasses.implementations.stdlib_rationals