proposition: Lemma up_logP p n : 1 < p -> n <= p ^ up_log p n.
proof: Proof. case: n => [|[|n]] // p_gt1; first by rewrite up_log1. by have /andP[] := up_log_bounds p_gt1 (isT: 1 < n.+2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)