proposition: Lemma Riemann_integrable_linear : forall (f g:R -> R) (a b l:R), Riemann_integrable f a b -> Riemann_integrable g a b -> Riemann_integrable (fun x:R => f x + l * g x) a b.
proof: Proof. apply RiemannInt_P10. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality