proposition: Lemma astab1R x : 'C[x | 'R] = 1.
proof: Proof. apply/trivgP/subsetP=> y cxy. by rewrite -(mulKg x y) [x * y](astab1P cxy) mulVg set11. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)