proposition: Lemma partnX pi m n : (m ^ n)`_pi = m`_pi ^ n.
proof: Proof. elim: n => [|n IHn]; first exact: partn1. rewrite expnS; have [->|m_gt0] := posnP m; first by rewrite partn0 exp1n. by rewrite expnS partnM ?IHn // expn_gt0 m_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)