proposition: Lemma primes_part pi n : primes n`_pi = filter [in pi] (primes n).
proof: Proof. have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0. apply: (irr_sorted_eq ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=. apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]]. rewrite /partn; apply big_ind => [|n1 n2 IHn1 IHn2|q pi_q]. - by rewrite dvdn1; case: eqP p_pr => // ->. - by rewrite Euclid_dvdM //; case/orP. rewrite -{1}(expn1 p) pfactor_dvdn // lognX muln_gt0. rewrite logn_gt0 mem_primes n_gt0 - andbA /=; case/and3P=> pr_q dv_q_n. by rewrite logn_prime //; case: eqP => // ->. have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq. rewrite [n`_pi]big_mkord (bigD1 (Ordinal le_p_n)) //= dvdn_mulr //. by rewrite lognE p_pr n_gt0 dv_p_n expnS dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)