proposition: Lemma compl_pHall pi K H G : pi.-Hall(G) K -> (H \in [complements to K in G]) = pi^'.-Hall(G) H.
proof: Proof. move=> hallK; apply/complP/idP=> [[tiKH mulKH] | hallH]. have [_] := andP hallK; rewrite /pHall pnatNK -{3}(invGid G) -mulKH mulG_subr. by rewrite invMG !indexMg -indexgI andbC -indexgI setIC tiKH !indexg1. have [[sKG piK _] [sHG pi'H _]] := (and3P hallK, and3P hallH). have tiKH: K :&: H = 1 := coprime_TIg (pnat_coprime piK pi'H). split=> //; apply/eqP; rewrite eqEcard mul_subG //= TI_cardMg //. by rewrite (card_Hall hallK) (card_Hall hallH) partnC. 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)