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