proposition: Lemma actby_is_action : is_action A (actby nRA).
proof: Proof. rewrite /actby; split=> [a x y | x a b Aa Ab /=]; last first. rewrite Aa Ab groupM // !andbT actMin ?(subsetP (acts_dom nRA)) //. by case Rx: (x \in R); rewrite ?(acts_act nRA) ?Rx. case Aa: (a \in A); rewrite ?andbF ?andbT //. case Rx: (x \in R); case Ry: (y \in R) => // eqxy; first exact: act_inj eqxy. by rewrite -eqxy (acts_act nRA Aa) Rx in Ry. by rewrite eqxy (acts_act nRA Aa) Ry in Rx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)