proposition: Lemma partn_pi n : n > 0 -> n`_\pi(n) = n.
proof: Proof. move=> n_gt0; rewrite [RHS]prod_prime_decomp // prime_decompE big_map. by rewrite -[n`__]big_filter filter_pi_of. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)