proposition: Lemma trunc_log_up_log p n : 1 < p -> 0 < n -> trunc_log p n = (up_log p n.+1).-1.
proof: Proof. by move=> ? ?; rewrite up_log_trunc_log. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)