proposition: Lemma StepFun_P41 : forall (f:R -> R) (a b c:R), a <= b -> b <= c -> IsStepFun f a b -> IsStepFun f b c -> IsStepFun f a c.
proof: Proof. intros f a b c H H0 (l1,(lf1,H1)) (l2,(lf2,H2)); destruct (total_order_T a b) as [[Hltab|Hab]|Hgtab]. - destruct (total_order_T b c) as [[Hltbc|Hbc]|Hgtbc]. + exists (app l1 l2); exists (FF (app l1 l2) f); apply StepFun_P40 with b lf1 lf2; assumption. + exists l1; exists lf1; rewrite Hbc in H1; assumption. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgtbc)). - exists l2; exists lf2; rewrite <- Hab in H2; assumption. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgtab)). Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra