proposition: Lemma Frobenius_actionP G H : reflect (has_Frobenius_action G H) [Frobenius G with complement H].
proof: Proof. apply: (iffP andP) => [[neqHG] | [sT S to [ffulG transG regG ntH [u Su defH]]]]. case/normedTI_P=> nzH /subsetIP[sHG _] tiHG. suffices: Frobenius_action G H (rcosets H G) 'Rs by apply: hasFrobeniusAction. pose Hfix x := 'Fix_(rcosets H G | 'Rs)[x]. have regG: {in G^#, forall x, #|Hfix x| <= 1}. move=> x /setD1P[ntx Gx]. apply: wlog_neg; rewrite -ltnNge => /ltnW/card_gt0P/=[Hy]. rewrite -(cards1 Hy) => /setIP[/imsetP[y Gy ->{Hy}] cHyx]. apply/subset_leq_card/subsetP=> _ /setIP[/imsetP[z Gz ->] cHzx]. rewrite -!sub_astab1 !astab1_act !sub1set astab1Rs in cHyx cHzx *. rewrite !rcosetE; apply/set1P/rcoset_eqP; rewrite mem_rcoset. apply: tiHG; [by rewrite !in_group | apply/pred0Pn; exists (x ^ y^-1)]. by rewrite conjD1g !inE conjg_eq1 ntx -mem_conjg cHyx conjsgM memJ_conjg. have ntH: H :!=: 1 by rewrite -subG1 -setD_eq0. split=> //; first 1 last; first exact: transRs_rcosets. by exists (val H); rewrite ?orbit_refl // astab1Rs (setIidPr sHG). apply/subsetP=> y /setIP[Gy cHy]; apply: contraR neqHG => nt_y. rewrite (index1g sHG) //; apply/eqP; rewrite eqn_leq indexg_gt0 andbT. apply: leq_trans (regG y _); last by rewrite setDE 2!inE Gy nt_y /=. by rewrite /Hfix (setIidPl _) -1?astabC ?sub1set. have sHG: H \subset G by rewrite defH subsetIl. split. apply: contraNneq ntH => /= defG. suffices defS: S = [set u] by rewrite -(trivgP ffulG) /= defS defH. apply/eqP; rewrite eq_sym eqEcard sub1set Su. by rewrite -(atransP transG u Su) card_orbit -defH defG indexgg cards1. apply/normedTI_P; rewrite setD_eq0 subG1 normD1 subsetI sHG normG. split=> // x Gx; rewrite -setI_eq0 conjD1g defH inE Gx conjIg conjGid //. rewrite -setDIl -setIIr -astab1_act setDIl => /set0Pn[y /setIP[Gy /setD1P[_]]]. case/setIP; rewrite 2!(sameP astab1P afix1P) => cuy cuxy; apply/astab1P. apply: contraTeq (regG y Gy) => cu'x. rewrite (cardD1 u) (cardD1 (to u x)) inE Su cuy inE /= inE cu'x cuxy. by rewrite (actsP (atrans_acts transG)) ?Su. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)