proposition: Lemma trunc_log_eq0 p n : (trunc_log p n == 0) = (p <= 1) || (n <= p.-1).
proof: Proof. case: p => [|[|p]]; case: n => // n; rewrite /= ltnS. have /= /andP[] := trunc_log_bounds (isT : 1 < p.+2) (isT : 0 < n.+1). case: trunc_log => [//|k] b1 b2. apply/idP/idP => [/eqP sk0 | nlep]; first by move: b2; rewrite sk0. symmetry; rewrite -[_ == _]/false /is_true -b1; apply/negbTE; rewrite -ltnNge. move: nlep; rewrite -ltnS => nlep; apply: (leq_ltn_trans nlep). by rewrite -[leqLHS]expn1; apply: leq_pexp2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)