proposition: Lemma up_log_trunc_log p n : 1 < p -> 1 < n -> up_log p n = (trunc_log p n.-1).+1.
proof: Proof. move=> p_gt1 n_gt1; apply: up_log_eq => //. rewrite -[n]prednK ?ltnS -?pred_Sn ?[0 < n]ltnW//. by rewrite trunc_logP ?ltn_predRL// trunc_log_ltn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)