proposition: Lemma StepFun_P19 : forall (l1:list R) (f g:R -> R) (l:R), Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 = Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1.
proof: Proof. intros; induction l1 as [| r l1 Hrecl1]; [ simpl; ring | induction l1 as [| r0 l1 Hrecl0]; simpl; [ ring | simpl in Hrecl1; rewrite Hrecl1; ring ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra