proposition: Lemma sorted_filter_le x s : sorted <=%O s -> [seq y <- s | y <= x] = take (count (<= x) s) s.
proof: Proof. elim: s => [//|y s IHs]/=; rewrite (path_sortedE le_trans) => /andP[le_y_s ss]. case: ifP => [|leyxF]; rewrite IHs//. rewrite (@eq_in_count _ _ pred0) ?count_pred0/= ?take0// => z. by move=> /(allP le_y_s) yz; apply: contraFF leyxF; apply: le_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)