proposition: Lemma trunc_log_eq p n k : 1 < p -> p ^ n <= k < p ^ n.+1 -> trunc_log p k = n.
proof: Proof. move=> p_gt1 /andP[npLk kLpn]; apply/anti_leq. rewrite trunc_log_max// andbT -ltnS -(ltn_exp2l _ _ p_gt1). apply: leq_ltn_trans kLpn; apply: trunc_logP => //. by apply: leq_trans npLk; rewrite expn_gt0 ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)