proposition: Lemma commG1P A B : reflect ([~: A, B] = 1) (A \subset 'C(B)).
proof: Proof. apply: (iffP (centsP A B)) => [cAB | cAB1 x Ax y By]. apply/trivgP; rewrite gen_subG; apply/subsetP=> _ /imset2P[x y Ax Ay ->]. by rewrite inE; apply/commgP; apply: cAB. by apply/commgP; rewrite -in_set1 -[[set 1]]cAB1 mem_commg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)