proposition: Lemma gcore_norm A G : G \subset 'N(gcore A G).
proof: Proof. apply/subsetP=> x Gx; rewrite inE; apply/bigcapsP=> y Gy. by rewrite sub_conjg -conjsgM bigcap_inf ?groupM ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)