proposition: Lemma Riemann_integrable_scal : forall (f : R -> R) (a b c : R), Riemann_integrable f a b -> Riemann_integrable (fun x => c * f x) a b.
proof: Proof. intros f a b c pr_f. apply (Riemann_integrable_ext (fun x => 0 + c * f x)). intros ; ring. apply (RiemannInt_P10 (c) (Riemann_integrable_const _ _ _) pr_f). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)