proposition: Lemma Riemann_integrable_bound (f : R -> R) (a b : R) : Riemann_integrable f a b -> exists s : R, forall x, Rmin a b <= x <= Rmax a b -> f x <= s.
proof: Proof. move => pr ; case (pr (mkposreal _ Rlt_0_1)) => {pr} phi [psi [pr _]] ; case: (StepFun_bound phi) => M_phi H_phi ; case: (StepFun_bound psi) => M_psi H_psi ; exists (M_psi + M_phi) => x Hx. apply Rle_trans with (2 := Rplus_le_compat _ _ _ _ (H_psi _ Hx) (H_phi _ Hx)). have: (f x = (f x - phi x) + phi x) ; first by ring. move => -> ; apply Rplus_le_compat_r, Rle_trans with (1 := Rle_abs _), pr, Hx. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)