proposition: Lemma gactsM (N1 N2 : {set rT}) : N1 \subset D -> N2 \subset D -> [acts A, on N1 | to] -> [acts A, on N2 | to] -> [acts A, on N1 * N2 | to].
proof: Proof. move=> sN1D sN2D aAN1 aAN2; apply/gactsP=> x Ax y. apply/idP/idP; case/mulsgP=> y1 y2 N1y1 N2y2 e. move: (actKin to Ax y); rewrite e; move<-. rewrite gactM ?groupV ?(subsetP sN1D y1) ?(subsetP sN2D) //. by apply: mem_mulg; rewrite ?(gactsP _ aAN1) ?(gactsP _ aAN2) // groupV. rewrite e gactM // ?(subsetP sN1D y1) ?(subsetP sN2D) //. by apply: mem_mulg; rewrite ?(gactsP _ aAN1) // ?(gactsP _ aAN2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)