proposition: Lemma injm_Frobenius_ker K sGD injf : [Frobenius G with kernel K] -> [Frobenius f @* G with kernel f @* K].
proof: Proof. case/existsP=> H frobG; apply/existsP. by exists (f @* H)%G; apply: injm_Frobenius. 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)