proposition: Lemma astab_trans_gcore G S u : [transitive G, on S | to] -> u \in S -> 'C(S | to) = gcore 'C[u | to] G.
proof: Proof. move=> transG Su; apply/eqP; rewrite eqEsubset. rewrite gcore_max ?astabS ?sub1set //=; last first. exact: subset_trans (atrans_acts transG) (astab_norm _ _). apply/subsetP=> x cSx; apply/astabP=> uy. case/(atransP2 transG Su) => y Gy ->{uy}. by apply/astab1P; rewrite astab1_act (bigcapP cSx). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)