proposition: Lemma trunc_log_max p k j : 1 < p -> p ^ j <= k -> j <= trunc_log p k.
proof: Proof. move=> p_gt1 le_pj_k; rewrite -ltnS -(@ltn_exp2l p) //. exact: leq_ltn_trans (trunc_log_ltn _ _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)