proposition: Lemma pfactor_dvdnn p n : p ^ logn p n %| n.
proof: Proof. case: n => // n; case pr_p: (prime p); first by rewrite pfactor_dvdn. by rewrite lognE pr_p dvd1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)