proposition: Lemma sub_gcore A B G : G \subset 'N(B) -> (B \subset gcore A G) = (B \subset A).
proof: Proof. move=> nBG; apply/idP/idP=> [sBAG | sBA]; last exact: gcore_max. exact: subset_trans (gcore_sub A G). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)