proposition: Lemma coprime_mulpG_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 piK pi'R; apply/andP. rewrite /pHall piK -!divgS /= -defG ?mulG_subl ?mulg_subr //= pnatNK. by rewrite coprime_cardMg ?(pnat_coprime piK) // mulKn ?mulnK //; apply/and3P. 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)