proposition: Lemma part_p'nat pi n : pi^'.-nat n -> n`_pi = 1.
proof: Proof. case/andP=> n_gt0 pi'_n; apply: big1_seq => p /andP[pi_p _]. by have [-> //|] := posnP (logn p n); rewrite logn_gt0; case/(allP pi'_n)/negP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)