proposition: Lemma StepFun_P2 : forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> adapted_couple f b a l lf.
proof: Proof. unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. - rewrite H2; unfold Rmin; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. + apply Rle_antisym; assumption. + apply Rle_antisym; auto with real. - rewrite H1; unfold Rmax; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. + apply Rle_antisym; assumption. + apply Rle_antisym; auto with real. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra