proposition: Lemma pprodJ A B x : pprod A B :^ x = pprod (A :^ x) (B :^ x).
proof: Proof. rewrite /pprod !conjsg_eq1 !group_setJ normJ conjSg -conjsMg. by do 3?case: ifP => // _; apply: conj0g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)