proposition: Lemma centU A B : 'C(A :|: B) = 'C(A) :&: 'C(B).
proof: Proof. apply/eqP; rewrite eqEsubset subsetI 2?centS ?(subsetUl, subsetUr) //=. by rewrite centsC subUset -centsC subsetIl -centsC subsetIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)