proposition: Lemma centJ A x : 'C(A :^ x) = 'C(A) :^ x.
proof: Proof. apply/setP=> y; rewrite mem_conjg; apply/centP/centP=> cAy z Az. by apply: (conjg_inj x); rewrite 2!conjMg conjgKV cAy ?memJ_conjg. by apply: (conjg_inj x^-1); rewrite 2!conjMg cAy -?mem_conjg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)