proposition: Lemma index_inside_r (a w : Q) (k : nat) (n : positive) : 0 ≤ w -> k < Pos.to_nat n -> a + (k : Q) * step w n ≤ a + w.
proof: Proof. intros A1 A2. apply (orders.order_preserving (a +)). mc_setoid_replace w with ((inject_Z n : Q) * (step w n)) at 2 by (symmetry; apply step_mult). apply (orders.order_preserving (.* step w n)). rewrite <- Zle_Qle, <- positive_nat_Z. apply inj_le. change (k ≤ Pos.to_nat n). solve_propholds. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration