proposition: Lemma partp_dvdn p (Hprime : prime p) n m : (0 < n) -> (p ^ m %| n) -> p ^ m %| n`_p .
proof: Proof. by move => Hn Hdiv; rewrite -(pfactorK m Hprime) -p_part partn_dvd. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)