proposition: Lemma acts_joing A M N : M \subset R -> N \subset R -> [acts A, on M | to] -> [acts A, on N | to] -> [acts A, on M <*> N | to].
proof: Proof. by move=> sMR sNR nMA nNA; rewrite acts_gen ?actsU // subUset sMR. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)