proposition: Lemma lt_sorted_ltn_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. move=> ss; have := lt_sorted_leq_nth x0 ss. exact: (anti_mono_in _ ltn_neqAle lt_neqAle anti_leq). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)