proposition: Lemma Riemann_sums_approximate_integral' (a : Q) (w : QnonNeg) (e : Qpos) (n : positive) : (step (proj1_sig w) n <= lmu a (proj1_sig w) (proj1_sig e))%Qinf -> ball (proj1_sig e * proj1_sig w) (riemann_sum a (proj1_sig w) n) (∫ f a w).
proof: Proof. intro A; unfold riemann_sum. destruct (Pos2Nat.is_succ n) as [m M]. rewrite M. apply Riemann_sums_approximate_integral; [rewrite <- M | easy]. unfold step. change (Pos.to_nat n * (proj1_sig w * (1 # n)) == proj1_sig w). rewrite positive_nat_Z. unfold inject_Z. rewrite Qmult_comm, <- Qmult_assoc. setoid_replace ((1 # n) * (n # 1)) with (1#1) by reflexivity. ring. 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