proposition: Lemma up_expnK p n : 1 < p -> up_log p (p ^ n) = n.
proof: Proof. case: n => [|n] p_gt1 /=; first by rewrite up_log1. by apply: up_log_eq; rewrite // leqnn andbT ltn_exp2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)