proposition: Lemma pnat_div m n pi : m %| n -> pi.-nat n -> pi.-nat (n %/ m).
proof: Proof. case/dvdnP=> q ->; rewrite pnatM andbC => /andP[]. by case: m => // m _; rewrite mulnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)