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