proposition: Lemma StepFun_P46 : forall (f:R -> R) (a b c:R), IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.
proof: Proof. intros f; intros; case (Rle_dec a b); case (Rle_dec b c); intros. - apply StepFun_P41 with b; assumption. - case (Rle_dec a c); intro. + apply StepFun_P44 with b; try assumption. split; [ assumption | auto with real ]. + apply StepFun_P6; apply StepFun_P44 with b. * apply StepFun_P6; assumption. * split; auto with real. - case (Rle_dec a c); intro. + apply StepFun_P45 with b; try assumption. split; auto with real. + apply StepFun_P6; apply StepFun_P45 with b. * apply StepFun_P6; assumption. * split; [ assumption | auto with real ]. - apply StepFun_P6; apply StepFun_P41 with b; auto with real || apply StepFun_P6; assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra