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