proposition: Lemma ex_maxnormal_ntrivg G : G :!=: 1-> {N : {group gT} | maxnormal N G G}.
proof: Proof. move=> ntG; apply: ex_maxgroup; exists [1 gT]%G; rewrite norm1 proper1G. by rewrite subsetT ntG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)