proposition: Lemma nth_count_ge x x0 s i : sorted <=%O s -> (count (< x) s <= i < size s)%N -> x <= nth x0 s i.
proof: Proof. move=> ss /andP[ige ilt]; rewrite -(subnKC ige) -nth_drop -sorted_filter_ge //. apply/(all_nthP _ (filter_all _ _)). by rewrite size_filter ltn_subLR // count_lt_ge subnK // count_size. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)