proposition: Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n.
proof: Proof. move=> n_gt0; rewrite -[RHS]partnT /partn //. do 2!rewrite mulnC big_mkcond /=; rewrite -big_split; apply: eq_bigr => p _ /=. by rewrite mulnC inE /=; case: (p \in pi); rewrite /= (muln1, mul1n). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)