proposition: Lemma StepFun_P16 : forall (f:R -> R) (l lf:list R) (a b:R), adapted_couple f a b l lf -> exists l' : list R, (exists lf' : list R, adapted_couple_opt f a b l' lf').
proof: Proof. intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply (StepFun_P10 Hle H) | assert (H1 : b <= a); [ auto with real | assert (H2 := StepFun_P10 H1 (StepFun_P2 H)); elim H2; intros l' [lf' H3]; exists l'; exists lf'; apply StepFun_P12; assumption ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra