proposition: Lemma partnM pi m n : m > 0 -> n > 0 -> (m * n)`_pi = m`_pi * n`_pi.
proof: Proof. have le_pmul m' n': m' > 0 -> n' <= m' * n' by move/prednK <-; apply: leq_addr. move=> mpos npos; rewrite !(@widen_partn (n * m)) 3?(le_pmul, mulnC) //. rewrite !big_mkord -big_split; apply: eq_bigr => p _ /=. by rewrite lognM // expnD. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)