proposition: Lemma trunc_expnK p n : 1 < p -> trunc_log p (p ^ n) = n.
proof: Proof. by move=> ?; apply: trunc_log_eq; rewrite // leqnn ltn_exp2l /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)