proposition: Lemma prim_trans_norm (H : {group aT}) : [primitive G, on S | to] -> H <| G -> H \subset 'C_G(S | to) \/ [transitive H, on S | to].
proof: Proof. move=> primG /andP[sHG nHG]; rewrite subsetI sHG. have [trG _] := andP primG; have [x Sx defS] := imsetP trG. move: primG; rewrite (trans_prim_astab Sx) // => /maximal_eqP[_]. case/(_ ('C_G[x | to] <*> H)%G) => /= [||cxH|]; first exact: joing_subl. - by rewrite join_subG subsetIl. - have{} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. rewrite subsetI sHG /= in cxH; left; apply/subsetP=> a Ha. apply/astabP=> y Sy; have [b Gb ->] := atransP2 trG Sx Sy. rewrite actCJV [to x (a ^ _)](astab1P _) ?(subsetP cxH) //. by rewrite -mem_conjg (normsP nHG). rewrite norm_joinEl 1?subIset ?nHG //. by move/(subgroup_transitiveP Sx sHG trG); right. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)