proposition: Lemma trunc_log_bounds p n : 1 < p -> 0 < n -> let k := trunc_log p n in p ^ k <= n < p ^ k.+1.
proof: Proof. rewrite {+}/trunc_log => p_gt1; have p_gt0 := ltnW p_gt1. rewrite [p <= 1]leqNgt p_gt1 /=. set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m. have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _. have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //. by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)