proposition: Lemma StepFun_P1 : forall (a b:R) (f:StepFun a b), adapted_couple f a b (subdivision f) (subdivision_val f).
proof: Proof. intros a b f; unfold subdivision_val; case (projT2 (pre f)) as (x,H); apply H. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra