proposition: Lemma astabs_range : 'N(R | to) = D.
proof: Proof. apply/setIidPl; apply/subsetP=> a Da; rewrite inE. by apply/subsetP=> x Rx; rewrite inE gact_stable. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)