proposition: Lemma cents_cycle x y : commute x y -> <[x]> \subset 'C(<[y]>).
proof: Proof. by move=> cxy; rewrite cent_cycle cycle_subG; apply/cent1P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)