proposition: Lemma actbyE x a : x \in R -> a \in A -> <[nRA]>%act x a = to x a.
proof: Proof. by rewrite /= /actby => -> ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)