proposition: Lemma astabRs_rcosets H G : 'C(rcosets H G | 'Rs) = gcore H G.
proof: Proof. have transGH := transRs_rcosets H G. by rewrite (astab_trans_gcore transGH (orbit_refl _ G _)) astab1Rs. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)