proposition: Lemma pdiv_pfactor p k : prime p -> pdiv (p ^ k.+1) = p.
proof: Proof. by move=> p_pr; rewrite /pdiv primesX ?primes_prime. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)