proposition: Lemma modact_coset_astab x a : a \in D -> (to %% 'C(R | to))%act x (coset _ a) = to x a.
proof: Proof. move=> Da; apply: modgactE => {x}//. rewrite !inE Da; apply/subsetP=> _ /imsetP[c Cc ->]. have Dc := astab_dom Cc; rewrite !inE groupJ //. apply/subsetP=> x Rx; rewrite inE conjgE !actMin ?groupM ?groupV //. by rewrite (astab_act Cc) ?actKVin // gact_stable ?groupV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)