proposition: Lemma dvdn_leq_log p m n : 0 < n -> m %| n -> logn p m <= logn p n.
proof: Proof. move=> n_gt0 dv_m_n; have m_gt0 := dvdn_gt0 n_gt0 dv_m_n. case p_pr: (prime p); last by do 2!rewrite lognE p_pr /=. by rewrite -pfactor_dvdn //; apply: dvdn_trans dv_m_n; rewrite pfactor_dvdn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)