proposition: Lemma StepFun_P29 : forall (a b:R) (f:StepFun a b), is_subdivision f a b (subdivision f).
proof: Proof. intros a b f; unfold is_subdivision; apply existT with (subdivision_val f); apply StepFun_P1. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra