proposition: Lemma trunc_logMp p n : 1 < p -> 0 < n -> trunc_log p (p * n) = (trunc_log p n).+1.
proof: Proof. case: p => [//|p] => p_gt0 n_gt0; apply: trunc_log_eq => //. rewrite expnS leq_pmul2l// trunc_logP//=. by rewrite expnS ltn_pmul2l// trunc_log_ltn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)