proposition: Lemma trans_prim_astab x : x \in S -> [transitive G, on S | to] -> [primitive G, on S | to] = maximal_eq 'C_G[x | to] G.
proof: Proof. move=> Sx trG; rewrite /primitive trG negb_exists. apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q]. split=> [|H sCH sHG]; first exact: subsetIl. pose X := orbit to H x; pose Q := orbit (to^*)%act G X. have Xx: x \in X by apply: orbit_refl. have defH: 'N_(G)(X | to) = H. have trH: [transitive H, on X | to] by apply/imsetP; exists x. have sHN: H \subset 'N_G(X | to) by rewrite subsetI sHG atrans_acts. move/(subgroup_transitiveP Xx sHN): (trH) => /= <-. by rewrite mulSGid //= setIAC subIset ?sCH. apply/imsetP; exists x => //; apply/eqP. by rewrite eqEsubset imsetS // acts_sub_orbit ?subsetIr. have [|/proper_card oCH] := eqVproper sCH; [by left | right]. apply/eqP; rewrite eqEcard sHG leqNgt. apply: contra {primG}(primG Q) => oHG; apply/and3P; split; last first. - rewrite card_orbit astab1_set defH -(@ltn_pmul2l #|H|) ?Lagrange // muln1. rewrite oHG -(@ltn_pmul2l #|H|) ?Lagrange // -(card_orbit_stab to G x). by rewrite -(atransP trG x Sx) mulnC card_orbit ltn_pmul2r. - by apply/actsP=> a Ga Y; apply/orbit_transl/mem_orbit. apply/and3P; split; last 1 first. - rewrite orbit_sym; apply/imsetP=> [[a _]] /= defX. by rewrite defX /setact imset0 inE in Xx. - apply/eqP/setP=> y; apply/bigcupP/idP=> [[_ /imsetP[a Ga ->]] | Sy]. case/imsetP=> _ /imsetP[b Hb ->] ->. by rewrite !(actsP (atrans_acts trG)) //; apply: subsetP Hb. case: (atransP2 trG Sx Sy) => a Ga ->. by exists ((to^*)%act X a); apply: imset_f; rewrite // orbit_refl. apply/trivIsetP=> _ _ /imsetP[a Ga ->] /imsetP[b Gb ->]. apply: contraR => /exists_inP[_ /imsetP[_ /imsetP[a1 Ha1 ->] ->]]. case/imsetP=> _ /imsetP[b1 Hb1 ->] /(canLR (actK _ _)) /(canLR (actK _ _)). rewrite -(canF_eq (actKV _ _)) -!actM (sameP eqP astab1P) => /astab1P Cab. rewrite astab1_set (subsetP (subsetIr G _)) //= defH. rewrite -(groupMr _ (groupVr Hb1)) -mulgA -(groupMl _ Ha1). by rewrite (subsetP sCH) // inE Cab !groupM ?groupV // (subsetP sHG). apply/and3P=> [[/and3P[/eqP defS tIQ ntQ]]]; set sto := (to^*)%act => actQ. rewrite !ltnNge -negb_or => /orP[]. pose X := pblock Q x; have Xx: x \in X by rewrite mem_pblock defS. have QX: X \in Q by rewrite pblock_mem ?defS. have toX Y a: Y \in Q -> a \in G -> to x a \in Y -> sto X a = Y. move=> QY Ga Yxa; rewrite -(contraNeq (trivIsetP tIQ Y (sto X a) _ _)) //. by rewrite (actsP actQ). by apply/existsP; exists (to x a); rewrite /= Yxa; apply: imset_f. have defQ: Q = orbit (to^*)%act G X. apply/eqP; rewrite eqEsubset andbC acts_sub_orbit // QX. apply/subsetP=> Y QY. have /set0Pn[y Yy]: Y != set0 by apply: contraNneq ntQ => <-. have Sy: y \in S by rewrite -defS; apply/bigcupP; exists Y. have [a Ga def_y] := atransP2 trG Sx Sy. by apply/imsetP; exists a; rewrite // (toX Y) // -def_y. rewrite defQ card_orbit; case: (maxCx 'C_G[X | sto]%G) => /= [||->|->]. - apply/subsetP=> a /setIP[Ga cxa]; rewrite inE Ga /=. by apply/astab1P; rewrite (toX X) // (astab1P cxa). - exact: subsetIl. - by right; rewrite -card_orbit (atransP trG). by left; rewrite indexgg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)