proposition: Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b.
proof: Proof. intros; unfold IsStepFun; destruct (Rle_dec a b) as [Hle|Hnle]. - apply existT with (cons a (cons b nil)); unfold is_subdivision; apply existT with (cons c nil); apply (StepFun_P3 c Hle). - apply existT with (cons b (cons a nil)); unfold is_subdivision; apply existT with (cons c nil); apply StepFun_P2; apply StepFun_P3; auto with real. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra