proposition: Lemma subcent1P A x y : reflect (y \in A /\ commute x y) (y \in 'C_A[x]).
proof: Proof. rewrite inE; case: (y \in A); last by right; case. by apply: (iffP cent1P) => [|[]]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)