proposition: Lemma StepFun_P15 : forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.
proof: Proof. intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply (StepFun_P14 Hle H H0) | assert (H1 : b <= a); [ auto with real | eapply StepFun_P14; [ apply H1 | apply StepFun_P2; apply H | apply StepFun_P12; apply H0 ] ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra