proposition: Lemma StepFun_P6 : forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a.
proof: Proof. unfold IsStepFun; intros; elim X; intros; apply existT with x; apply StepFun_P5; assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra