proposition: Lemma properG_ltn_log p G H : p.-group G -> H \proper G -> logn p #|H| < logn p #|G|.
proof: Proof. move=> pG; rewrite properEneq eqEcard andbC ltnNge => /andP[sHG]. rewrite sHG /= {1}(card_pgroup pG) {1}(card_pgroup (pgroupS sHG pG)). by apply: contra; case: p {pG} => [|p] leHG; rewrite ?logn0 // leq_pexp2l. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)