proposition: Lemma conjsRg A B x : [~: A, B] :^ x = [~: A :^ x, B :^ x].
proof: Proof. wlog suffices: A B x / [~: A, B] :^ x \subset [~: A :^ x, B :^ x]. move=> subJ; apply/eqP; rewrite eqEsubset subJ /= -sub_conjgV. by rewrite -{2}(conjsgK x A) -{2}(conjsgK x B). rewrite -genJ gen_subG; apply/subsetP=> _ /imsetP[_ /imset2P[y z Ay Bz ->] ->]. by rewrite conjRg mem_commg ?memJ_conjg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)