proposition: Lemma astab_range : 'C(R | to) = 'C(setT | to).
proof: Proof. apply/eqP; rewrite eqEsubset andbC astabS ?subsetT //=. apply/subsetP=> a cRa; have Da := astab_dom cRa; rewrite !inE Da. apply/subsetP=> x; rewrite -(setUCr R) !inE. by case/orP=> ?; [rewrite (astab_act cRa) | rewrite gact_out]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)