proposition: Lemma norms_bigcap I r (P : pred I) A (B_ : I -> {set gT}) : A \subset \bigcap_(i <- r | P i) 'N(B_ i) -> A \subset 'N(\bigcap_(i <- r | P i) B_ i).
proof: Proof. elim/big_rec2: _ => [|i B N _ IH /subsetIP[nBiA /IH]]; last exact: normsI. by rewrite normT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)