proposition: Lemma SymE : Sym S = 'C(~: S | 'P).
proof: Proof. apply/setP => s; rewrite inE; apply/idP/astabP => [sS x|/= S_id]. by rewrite inE /= apermE => /out_perm->. by apply/subsetP => x; move=> /(contra_neqN (S_id _)); rewrite inE negbK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)