proposition: Lemma sub_afixRs_norms G x A : (G :* x \in 'Fix_('Rs)(A)) = (A \subset G :^ x).
proof: Proof. rewrite inE /=; apply: eq_subset_r => a. rewrite inE rcosetE -(can2_eq (rcosetKV x) (rcosetK x)) -!rcosetM. rewrite eqEcard card_rcoset leqnn andbT mulgA (conjgCV x) mulgK. by rewrite -{2 3}(mulGid G) mulGS sub1set -mem_conjg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)