proposition: Lemma dvdn_partP n m : 0 < n -> reflect (forall p, p \in \pi(n) -> n`_p %| m) (n %| m).
proof: Proof. move=> n_gt0; apply: (iffP idP) => n_dvd_m => [p _|]. by apply: dvdn_trans n_dvd_m; apply: dvdn_part. have [-> // | m_gt0] := posnP m. rewrite -(partnT n_gt0) -(partnT m_gt0). rewrite !(@widen_partn (m + n)) ?leq_addl ?leq_addr // /in_mem /=. elim/big_ind2: _ => // [* | q _]; first exact: dvdn_mul. have [-> // | ] := posnP (logn q n); rewrite logn_gt0 => q_n. have pr_q: prime q by move: q_n; rewrite mem_primes; case/andP. by have:= n_dvd_m q q_n; rewrite p_part !pfactor_dvdn // pfactorK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)