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