proposition: Lemma StepFun_P27 : forall (a b l:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg).
proof: Proof. intros a b l f g lf lg H H0; apply StepFun_P26; [ apply StepFun_P23 with g; assumption | apply StepFun_P25 with f; assumption ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra