proposition: Lemma StepFun_P9 : forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> a <> b -> (2 <= length l)%nat.
proof: Proof. intros; unfold adapted_couple in H; decompose [and] H; clear H; induction l as [| r l Hrecl]. - simpl in H4; discriminate. - induction l as [| r0 l Hrecl0]; [ simpl in H3; simpl in H2; generalize H3; generalize H2; unfold Rmin, Rmax; case (Rle_dec a b); intros; elim H0; rewrite <- H5; rewrite <- H7; reflexivity | simpl; do 2 apply le_n_S; apply Nat.le_0_l ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra