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