proposition: Lemma StepFun_P25 : forall (a b:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg).
proof: Proof. intros a b f g lf lg H H0; case (Rle_dec a b); intro; [ apply StepFun_P24 with f; assumption | apply StepFun_P5; apply StepFun_P24 with f; [ auto with real | apply StepFun_P5; assumption | apply StepFun_P5; assumption ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra