proposition: Lemma gcore_max A B G : B \subset A -> G \subset 'N(B) -> B \subset gcore A G.
proof: Proof. move=> sBA nBG; apply/bigcapsP=> y Gy. by rewrite -sub_conjgV (normsP nBG) ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)