proposition: Lemma mingroupP : reflect (gP G /\ forall H, gP H -> H \subset G -> H :=: G) (mingroup G gP).
proof: Proof. apply: (iffP minsetP); rewrite /= groupP genGidG /= => [] [-> minG]. by split=> // H gPH sGH; apply: minG; rewrite // groupP genGidG. by split=> // A; case/andP=> gA gPA; rewrite -(gen_set_id gA); apply: minG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)