proposition: Lemma partn_part pi rho n : {subset pi <= rho} -> n`_rho`_pi = n`_pi.
proof: Proof. move=> pi_sub_rho; have [->|n_gt0] := posnP n; first by rewrite !partn0 partn1. rewrite -[in RHS](partnC rho n_gt0) partnM //. suffices: pi^'.-nat n`_rho^' by move/part_p'nat->; rewrite muln1. by apply: sub_in_pnat (part_pnat _ _) => q _; apply/contra/pi_sub_rho. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)