proposition: Lemma coprime_mulGp_Hall pi G K R : K * R = G -> pi^'.-group K -> pi.-group R -> pi^'.-Hall(G) K /\ pi.-Hall(G) R.
proof: Proof. move=> defG pi'K piR; apply/andP; rewrite andbC; apply/andP. by apply: coprime_mulpG_Hall => //; rewrite -(comm_group_setP _) defG ?groupP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)