proposition: Lemma trunc_log_gt0 p n : (0 < trunc_log p n) = (1 < p) && (p.-1 < n).
proof: Proof. by rewrite ltnNge leqn0 trunc_log_eq0 negb_or -!ltnNge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)