proposition: Lemma partnI pi rho n : n`_[predI pi & rho] = n`_pi`_rho.
proof: Proof. rewrite -(@partnC [predI pi & rho] _`_rho) //. symmetry; rewrite 2?partn_part; try by move=> p /andP []. rewrite mulnC part_p'nat ?mul1n // pnatNK pnatI part_pnat andbT. exact: pnat_dvd (dvdn_part _ _) (part_pnat _ _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)