proposition: Lemma class_support_sub_norm A B G : A \subset G -> B \subset 'N(G) -> class_support A B \subset G.
proof: Proof. move=> sAG nGB; rewrite class_supportEr. by apply/bigcupsP=> x Bx; rewrite -(normsP nGB x Bx) conjSg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)