proposition: Lemma centsS A B C : A \subset B -> C \subset 'C(B) -> C \subset 'C(A).
proof: Proof. by move=> sAB cCB; apply: subset_trans cCB (centS sAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)