proposition: Corollary Hall_trans pi (G H1 H2 : {group gT}) : solvable G -> pi.-Hall(G) H1 -> pi.-Hall(G) H2 -> exists2 x, x \in G & H1 :=: H2 :^ x.
proof: Proof. move=> solG; have [H hallH transH] := Hall_exists_subJ pi solG. have conjH (K : {group gT}): pi.-Hall(G) K -> exists2 x, x \in G & K = (H :^ x)%G. - move=> hallK; have [sKG piK _] := and3P hallK. case: (transH K sKG piK) => x Gx sKH; exists x => //. apply/eqP; rewrite -val_eqE eqEcard sKH cardJg. by rewrite (card_Hall hallH) (card_Hall hallK) /=. case/conjH=> x1 Gx1 ->{H1}; case/conjH=> x2 Gx2 ->{H2}. exists (x2^-1 * x1); first by rewrite groupMl ?groupV. by apply: val_inj; rewrite /= conjsgM conjsgK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)