proposition: Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n.
proof: Proof. case/andP=> n_gt0 pi_n; rewrite -[RHS]partnT // /partn big_mkcond /=. apply: eq_bigr=> p _; have [->|] := posnP (logn p n); first by rewrite if_same. by rewrite logn_gt0 => /(allP pi_n)/= ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)