proposition: Lemma up_log_eq0 p n : (up_log p n == 0) = (p <= 1) || (n <= 1).
proof: Proof. case: p => // [] [] // p. case: n => [|[|n]]; rewrite /up_log //=. have /= := trunc_log_bounds (isT : 1 < p.+2) (isT : 0 < n.+2). by case: (leqP _ n.+1); case: trunc_log. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)