proposition: Lemma acts_subnorm_fix A : [acts 'N_D(A), on 'Fix_to(D :&: A) | to].
proof: Proof. apply/subsetP=> a nAa; have [Da _] := setIP nAa; rewrite !inE Da. apply/subsetP=> x Cx /[1!inE]; apply/afixP=> b DAb. have [Db _]:= setIP DAb; rewrite -actMin // conjgCV actMin ?groupJ ?groupV //. by rewrite /= (afixP Cx) // memJ_norm // groupV (subsetP (normsGI _ _) _ nAa). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)