proposition: Theorem Gaschutz_transitive : {in [complements to H in G] &, forall K L, K :&: P = L :&: P -> exists2 x, x \in H & L :=: K :^ x}.
proof: Proof. move=> K L /=; set Q := K :&: P => /complP[tiHK eqHK] cpHL QeqLP. have [trHL eqHL] := complP cpHL. pose nu x := fmod (divgr H L x^-1). have sKG: {subset K <= G} by apply/subsetP; rewrite -eqHK mulG_subr. have sLG: {subset L <= G} by apply/subsetP; rewrite -eqHL mulG_subr. have val_nu x: x \in G -> val (nu x) = divgr H L x^-1. by move=> Gx; rewrite fmodK // mem_divgr // eqHL groupV. have nu_cocycle: {in G &, forall x y, nu (x * y)%g = nu x ^@ y + nu y}%R. move=> x y Gx Gy; apply: val_inj; rewrite fmvalA fmvalJ ?nHG //. rewrite !val_nu ?groupM // /divgr conjgE !mulgA mulgK. by rewrite !(invMg, remgrM cpHL) ?groupV ?mulgA. have nuL x: x \in L -> nu x = 0%R. move=> Lx; apply: val_inj; rewrite val_nu ?sLG //. by rewrite /divgr remgr_id ?groupV ?mulgV. exists (fmval ((\sum_(X in rcosets Q K) nu (repr X)) *+ m)). exact: fmodP. apply/eqP; rewrite eq_sym eqEcard; apply/andP; split; last first. by rewrite cardJg -(leq_pmul2l (cardG_gt0 H)) -!TI_cardMg // eqHL eqHK. apply/subsetP=> _ /imsetP[x Kx ->]; rewrite conjgE mulgA (conjgC _ x). have Gx: x \in G by rewrite sKG. rewrite conjVg -mulgA -fmvalJ ?nHG // -fmvalN -fmvalA (_ : _ + _ = nu x)%R. by rewrite val_nu // mulKVg groupV mem_remgr // eqHL groupV. rewrite actZr -!mulNrn -mulrnDl actr_sum. rewrite addrC (reindex_acts _ (actsRs_rcosets _ K) Kx) -sumrB /= -/Q. rewrite (eq_bigr (fun _ => nu x)) => [|_ /imsetP[y Ky ->]]; last first. rewrite !rcosetE -rcosetM QeqLP. case: repr_rcosetP => z /setIP[Lz _]; case: repr_rcosetP => t /setIP[Lt _]. rewrite !nu_cocycle ?groupM ?(sKG y) // ?sLG //. by rewrite (nuL z) ?(nuL t) // !act0r !add0r addrC addKr. apply: val_inj; rewrite sumr_const !fmvalZ. rewrite -{2}(expgK coHiPG (fmodP (nu x))); congr (_ ^+ _ ^+ _). rewrite -[#|_|]divgS ?subsetIl // -(divnMl (cardG_gt0 H)). rewrite -!TI_cardMg //; last by rewrite setIA setIAC (setIidPl sHP). by rewrite group_modl // eqHK (setIidPr sPG) divgS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)