proposition: Lemma astab_norm S : 'N(S | to) \subset 'N('C(S | to)).
proof: Proof. apply/subsetP=> a nSa; rewrite inE sub_conjg; apply/subsetP=> b cSb. have [Da Db] := (astabs_dom nSa, astab_dom cSb). rewrite mem_conjgV !inE groupJ //; apply/subsetP=> x Sx. rewrite inE !actMin ?groupM ?groupV //. by rewrite (astab_act cSb) ?actKVin ?astabs_act ?groupV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)