proposition: Lemma pnatM pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n.
proof: Proof. rewrite /pnat muln_gt0 andbCA -andbA andbCA. case: posnP => // n_gt0; case: posnP => //= m_gt0. apply/allP/andP=> [pi_mn | [pi_m pi_n] p]. by split; apply/allP=> p m_p; apply: pi_mn; rewrite primesM // m_p ?orbT. by rewrite primesM // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)