proposition: Lemma astabsD1 S : 'N(S^# | to) = 'N(S | to).
proof: Proof. case S1: (1 \in S); last first. by rewrite (setDidPl _) // disjoint_sym disjoints_subset sub1set inE S1. apply/eqP; rewrite eqEsubset andbC -{1}astabsIdom -{1}astabs1 setIC astabsD /=. by rewrite -{2}(setD1K S1) -astabsIdom -{1}astabs1 astabsU. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)