proposition: Lemma centP A x : reflect (centralises x A) (x \in 'C(A)).
proof: Proof. by apply: (iffP bigcapP) => cxA y /cxA/cent1P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)