proposition: Lemma ltn_odd_Frobenius_ker : odd #|G| -> #|H|.*2 < #|K|.
proof: Proof. move/oddSg=> oddG. have [/sdprodW/mulG_sub[sKG sHG] ntK _ _ _] := Frobenius_context. by rewrite dvdn_double_ltn ?oddG ?cardG_gt1 ?Frobenius_dvd_ker1. 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)