proposition: Lemma conjg_prod I r (P : pred I) F z : (\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
proof: Proof. by apply: (big_morph (conjg^~ z)) => [x y|]; rewrite ?conj1g ?conjMg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)