proposition: Lemma partnT n : n > 0 -> n`_predT = n.
proof: Proof. move=> n_gt0; rewrite -[RHS]partn_pi // [RHS]/partn big_mkcond /=. by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)