proposition: Lemma p_natP p n : p.-nat n -> {k | n = p ^ k}.
proof: Proof. by move=> p_n; exists (logn p n); rewrite -p_part part_pnat_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)