proposition: Lemma conjugates_conj A x B : (A :^ x) :^: B = A :^: (x *: B).
proof: Proof. rewrite /conjugates [x *: B]imset2_set1l -imset_comp. by apply: eq_imset => y /=; rewrite conjsgM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)