proposition: Lemma acts_subnorm_gacent A : A \subset D -> [acts 'N_D(A), on 'C_(| to)(A) | to].
proof: Proof. move=> sAD; rewrite gacentE // actsI ?astabs_range ?subsetIl //. by rewrite -{2}(setIidPr sAD) acts_subnorm_fix. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)