proposition: Lemma max_pdiv_dvd n : max_pdiv n %| n.
proof: Proof. by case: n (pi_max_pdiv n) => [|[|n]] //; rewrite mem_primes => /andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)