proposition: Lemma norms_bigcup I r (P : pred I) A (B_ : I -> {set gT}) : A \subset \bigcap_(i <- r | P i) 'N(B_ i) -> A \subset 'N(\bigcup_(i <- r | P i) B_ i).
proof: Proof. move=> nBA; rewrite -normCs setC_bigcup norms_bigcap //. by rewrite (eq_bigr _ (fun _ _ => normCs _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)