proposition: Lemma ltn_log0 p n : n < p -> logn p n = 0.
proof: Proof. by case: n => [|n] ltnp; rewrite lognE ?andbF // gtnNdvd ?andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)