proposition: Lemma norms_class_support : A \subset 'N(class_support B C).
proof: Proof. apply/subsetP=> x Ax; rewrite inE sub_conjg class_supportEr. apply/bigcupsP=> y Cy; rewrite -sub_conjg -conjsgM conjgC conjsgM. by rewrite (normsP nBA) // bigcup_sup ?memJ_norm ?(subsetP nCA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)