proposition: Lemma RiemannInt_P13 : 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. intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply RiemannInt_P12; assumption | assert (H : b <= a); [ auto with real | replace (RiemannInt pr3) with (- RiemannInt (RiemannInt_P1 pr3)); [ idtac | symmetry ; apply RiemannInt_P8 ]; replace (RiemannInt pr2) with (- RiemannInt (RiemannInt_P1 pr2)); [ idtac | symmetry ; apply RiemannInt_P8 ]; replace (RiemannInt pr1) with (- RiemannInt (RiemannInt_P1 pr1)); [ idtac | symmetry ; apply RiemannInt_P8 ]; rewrite (RiemannInt_P12 (RiemannInt_P1 pr1) (RiemannInt_P1 pr2) (RiemannInt_P1 pr3) H); ring ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra