proposition: Lemma injm_Frobenius_compl H sGD injf : [Frobenius G with complement H] -> [Frobenius f @* G with complement f @* H].
proof: Proof. case/andP=> neqGH /normedTI_P[nzH /subsetIP[sHG _] tiHG]. have sHD := subset_trans sHG sGD; have sH1D := subset_trans (subD1set H 1) sHD. apply/andP; rewrite (can_in_eq (injmK injf)) //; split=> //. apply/normedTI_P; rewrite normD1 -injmD1 // -!cards_eq0 card_injm // in nzH *. rewrite subsetI normG morphimS //; split=> // _ /morphimP[x Dx Gx ->] ti'fHx. rewrite mem_morphim ?tiHG //; apply: contra ti'fHx; rewrite -!setI_eq0 => tiHx. by rewrite -morphimJ // -injmI ?conj_subG // (eqP tiHx) morphim0. 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)