proposition: Lemma StepFun_P13 : forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a <> b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2.
proof: Proof. intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - eapply StepFun_P11; [ apply Hlt | apply H0 | apply H1 ]. - elim H; assumption. - eapply StepFun_P11; [ apply Hgt | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra