proposition: Lemma lognM p m n : 0 < m -> 0 < n -> logn p (m * n) = logn p m + logn p n.
proof: Proof. case p_pr: (prime p); last by rewrite /logn p_pr. have xlp := pfactor_coprime p_pr. case/xlp=> m' co_m' def_m /xlp[n' co_n' def_n] {xlp}. rewrite [in LHS]def_m [in LHS]def_n mulnCA -mulnA -expnD !logn_Gauss //. exact: pfactorK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)