fact: Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:list R) := adapted_couple f a b l lf /\ (forall i:nat, (i < pred (length lf))%nat -> pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\ (forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <> pos_Rl l (S i)).
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra