proposition: Lemma im_actm a : actm to a @* R = R.
proof: Proof. apply/eqP; rewrite eqEcard (card_injm (injm_actm a)) // leqnn andbT. apply/subsetP=> _ /morphimP[x Rx _ ->] /=. by rewrite /actm; case: ifP => // Da; rewrite gact_stable. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)