proposition: Lemma trunc_logP p n : 1 < p -> 0 < n -> p ^ trunc_log p n <= n.
proof: Proof. by move=> p_gt1 /(trunc_log_bounds p_gt1)/andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)