proposition: Lemma partn_eq1 pi n : n > 0 -> (n`_pi == 1) = pi^'.-nat n.
proof: Proof. move=> n_gt0; apply/eqP/idP=> [pi_n_1|]; last exact: part_p'nat. by rewrite -(partnC pi n_gt0) pi_n_1 mul1n part_pnat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)