proposition: Lemma partn_dvd pi m n : n > 0 -> m %| n -> m`_pi %| n`_pi.
proof: Proof. move=> n_gt0 dvmn; case/dvdnP: dvmn n_gt0 => q ->{n}. by rewrite muln_gt0 => /andP[q_gt0 m_gt0]; rewrite partnM ?dvdn_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)