proposition: Lemma filter_le_nth x0 s i : sorted <%O s -> (i < size s)%N -> [seq x <- s | x <= nth x0 s i] = take i.+1 s.
proof: Proof. move=> ss i_lt/=; rewrite -[X in filter _ X](mkseq_nth x0) filter_map. under eq_in_filter => j do [rewrite ?mem_iota => j_s /=; rewrite lt_sorted_leq_nth//]. by rewrite (filter_iota_leq 0)// map_nth_iota0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)