proposition: Lemma count_lt_nth x0 s i : sorted <%O s -> (i < size s)%N -> count (< nth x0 s i) s = i.
proof: Proof. by move=> ss i_lt; rewrite -size_filter/= filter_lt_nth// size_take i_lt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)