proposition: Lemma lt_sorted_leq_nth (x0 : T) (s : seq T) : sorted <%O s -> {in [pred n | (n < size s)%N] &, {mono nth x0 s : i j / (i <= j)%N >-> i <= j}}.
proof: Proof. rewrite lt_sorted_uniq_le => /andP[s_uniq le_s]. apply: (total_homo_mono_in _ _ ltn_neqAle lt_neqAle le_anti leq_total) => //. move=> i j ilt jlt ltij; rewrite lt_neqAle le_sorted_leq_nth// 1?ltnW//. by rewrite nth_uniq// ltn_eqF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)