proposition: Lemma StepFun_P30 : forall (a b l:R) (f g:StepFun a b), RiemannInt_SF (mkStepFun (StepFun_P28 l f g)) = RiemannInt_SF f + l * RiemannInt_SF g.
proof: Proof. intros a b l f g; unfold RiemannInt_SF; case (Rle_dec a b); (intro; replace (Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g))) (subdivision (mkStepFun (StepFun_P28 l f g)))) with (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) (fun x:R => f x + l * g x)) (cons_ORlist (subdivision f) (subdivision g))); [ rewrite StepFun_P19; replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val f) (subdivision f)); [ replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val g) (subdivision g)); [ ring | apply StepFun_P17 with (fe g) a b; [ apply StepFun_P1 | apply StepFun_P21; apply StepFun_P25 with (fe f); apply StepFun_P29 ] ] | apply StepFun_P17 with (fe f) a b; [ apply StepFun_P1 | apply StepFun_P21; apply StepFun_P23 with (fe g); apply StepFun_P29 ] ] | apply StepFun_P17 with (fun x:R => f x + l * g x) a b; [ apply StepFun_P21; apply StepFun_P27; apply StepFun_P29 | apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g))) ] ]). Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra