proposition: Lemma FrobeniusJ x G K H : [Frobenius G :^ x = K :^ x ><| H :^ x] = [Frobenius G = K ><| H].
proof: Proof. by congr (_ && _); rewrite ?FrobeniusJcompl // -sdprodJ (can_eq (conjsgK x)). 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)