proposition: Lemma maximal_exists H G : H \subset G -> H :=: G \/ (exists2 M : {group gT}, maximal M G & H \subset M).
proof: Proof. rewrite subEproper; case/predU1P=> sHG; first by left. suff [M *]: {M : {group gT} | maximal M G & H \subset M} by right; exists M. exact: maxgroup_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)