proposition: Lemma sorted_leq_index_in s : {in s & &, transitive leT} -> {in s, reflexive leT} -> sorted s -> {in s &, forall x y, index x s <= index y s -> leT x y}.
proof: Proof. case: s => // x0 s' leT_tr leT_refl s_sorted x y xs ys. move/(sorted_leq_nth_in leT_tr leT_refl x0 (allss (_ :: _)) s_sorted). by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)