proposition: Lemma lognX p m n : logn p (m ^ n) = n * logn p m.
proof: Proof. case p_pr: (prime p); last by rewrite /logn p_pr muln0. elim: n => [|n IHn]; first by rewrite logn1. have [->|m_gt0] := posnP m; first by rewrite exp0n // lognE andbF muln0. by rewrite expnS lognM ?IHn // expn_gt0 m_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)