proposition: Lemma logn_gt0 p n : (0 < logn p n) = (p \in primes n).
proof: Proof. by rewrite lognE -mem_primes; case: {+}(p \in _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)