proposition: Lemma astabR G : 'C(G | 'R) = 1.
proof: Proof. apply/trivgP/subsetP=> x cGx. by rewrite -(mul1g x) [1 * x](astabP cGx) group1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)