proposition: Lemma Frobenius_kerS G K G1 : G1 \subset G -> K \proper G1 -> [Frobenius G with kernel K] -> [Frobenius G1 with kernel K].
proof: Proof. move=> sG1G ltKG1 /Frobenius_kerP[ntK _ /andP[_ nKG] regKG]. apply/Frobenius_kerP; rewrite /normal proper_sub // (subset_trans sG1G) //. by split=> // x /regKG; apply: subset_trans; rewrite setSI. 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)