proposition: Lemma astabsR G : 'N(G | 'R) = G.
proof: Proof. apply/setP=> x; rewrite !inE -setactVin ?inE //=. by rewrite -groupV -{1 3}(mulg1 G) rcoset_sym -sub1set -mulGS -!rcosetE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)