proposition: Lemma astab1 : 'C(1 | to) = D.
proof: Proof. by apply/setP=> x; rewrite ?(inE, sub1set) andb_idr //; move/gact1=> ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)