proposition: Lemma Frobenius_context : [/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].
proof: Proof. have [/eqP defG neqHG ntH _] := and4P frobG; rewrite setD_eq0 subG1 in ntH. have ntK: K :!=: 1 by apply: contraNneq neqHG => K1; rewrite -defG K1 sdprod1g. rewrite properEcard properEneq neqHG; have /mulG_sub[-> ->] := sdprodW defG. by rewrite -(sdprod_card defG) ltn_Pmulr ?cardG_gt1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)