proposition: Lemma up_logMp p n : 1 < p -> 0 < n -> up_log p (p * n) = (up_log p n).+1.
proof: Proof. case: p => [//|p] p_gt0. case: n => [//|[|n]] _; first by rewrite muln1 up_lognn// up_log1. apply: up_log_eq => //. rewrite expnS leq_pmul2l// up_logP// andbT. rewrite -[up_log _ _]prednK ?up_log_gt0 ?p_gt0 //. by rewrite expnS ltn_pmul2l// up_log_gtn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)