proposition: Lemma lognE p m : logn p m = if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0.
proof: Proof. rewrite /logn /dvdn; case p_pr: (prime p) => //. case def_m: m => // [m']; rewrite !andTb [LHS]/= -def_m /divn modn_def. case: edivnP def_m => [[|q] [|r] -> _] // def_m; congr _.+1; rewrite [_.1]/=. have{m def_m}: q < m'. by rewrite -ltnS -def_m addn0 mulnC -{1}[q.+1]mul1n ltn_pmul2r // prime_gt1. elim/ltn_ind: m' {q}q.+1 (ltn0Sn q) => -[_ []|r IHr m] //= m_gt0 le_mr. rewrite -[m in logn_rec _ _ m]prednK //=. case: edivnP => [[|q] [|_] def_q _] //; rewrite addn0 in def_q. have{def_q} lt_qm1: q < m.-1. by rewrite -[q.+1]muln1 -ltnS prednK // def_q ltn_pmul2l // prime_gt1. have{le_mr} le_m1r: m.-1 <= r by rewrite -ltnS prednK. by rewrite (IHr r) ?(IHr m.-1) // (leq_trans lt_qm1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)