proposition: Lemma Riemann_integrable_scal : forall f a b k, Riemann_integrable f a b -> Riemann_integrable (fun x => k * f x) a b.
proof: Proof. intros f a b k ri. apply Riemann_integrable_ext with (f := fun x => 0 + k * f x). { intros; ring. } apply (RiemannInt_P10 _ (RiemannInt_P14 _ _ 0) ri). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra