proposition: Lemma up_log_bounds p n : 1 < p -> 1 < n -> let k := up_log p n in p ^ k.-1 < n <= p ^ k.
proof: Proof. move=> p_gt1 n_gt1. have n_gt0 : 0 < n by apply: leq_trans n_gt1. rewrite /up_log (leqNgt p 1) p_gt1 /=. have /= /andP[tpLn nLtpS] := trunc_log_bounds p_gt1 n_gt0. have [nLnp|npLn] := leqP n (p ^ trunc_log p n); last by rewrite npLn ltnW. rewrite nLnp (leq_trans _ tpLn) // ltn_exp2l // prednK ?leqnn //. by case: trunc_log (leq_trans n_gt1 nLnp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)