proposition: Lemma lognSg p G H : G \subset H -> logn p #|G| <= logn p #|H|.
proof: Proof. by move=> sGH; rewrite dvdn_leq_log ?cardSg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)