proposition: Lemma logn_div p m n : m %| n -> logn p (n %/ m) = logn p n - logn p m.
proof: Proof. rewrite dvdn_eq => /eqP def_n. case: (posnP n) => [-> |]; first by rewrite div0n logn0. by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)