proposition: Lemma injm_Frobenius H K sGD injf : [Frobenius G = K ><| H] -> [Frobenius f @* G = f @* K ><| f @* H].
proof: Proof. case/andP=> /eqP defG frobG. by apply/andP; rewrite (injm_sdprod _ injf defG) // eqxx injm_Frobenius_compl. 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)