proposition: Lemma StepFun_P23 : 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 f a b (cons_ORlist lf lg).
proof: Proof. intros; case (Rle_dec a b); intro; [ apply StepFun_P22 with g; assumption | apply StepFun_P5; apply StepFun_P22 with g; [ auto with real | apply StepFun_P5; assumption | apply StepFun_P5; assumption ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra