proposition: Lemma ltn_log_quotient : p.-group G -> H :!=: 1 -> H \subset G -> logn p #|G / H| < logn p #|G|.
proof: Proof. move=> pG ntH sHG; apply: contraLR (ltn_quotient ntH sHG); rewrite -!leqNgt. rewrite {2}(card_pgroup pG) {2}(card_pgroup (morphim_pgroup _ pG)). by case: (posnP p) => [-> //|]; apply: 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)