proposition: Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log p n).+1.
proof: Proof. have [-> | n_gt0] := posnP n; first by rewrite trunc_log0 => /ltnW. by case/trunc_log_bounds/(_ n_gt0)/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)