proposition: Lemma cent1P x y : reflect (commute x y) (x \in 'C[y]).
proof: Proof. rewrite [x \in _]inE conjg_set1 sub1set !inE (sameP eqP conjg_fixP)commg1_sym. exact: commgP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)