proposition: Lemma logn_Gauss p m n : coprime p m -> logn p (m * n) = logn p n.
proof: Proof. move=> co_pm; case p_pr: (prime p); last by rewrite /logn p_pr. have [-> | n_gt0] := posnP n; first by rewrite muln0. have [m0 | m_gt0] := posnP m; first by rewrite m0 prime_coprime ?dvdn0 in co_pm. have mn_gt0: m * n > 0 by rewrite muln_gt0 m_gt0. apply/eqP; rewrite eqn_leq andbC dvdn_leq_log ?dvdn_mull //. set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn. by rewrite Gauss_dvdr ?coprimeXl // -pfactor_dvdn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)