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