proposition: Lemma maxainv_exists : K :!=: 1 -> {N : {group rT} | maxainv K N}.
proof: Proof. move=> nt; apply: ex_maxgroup. exists [1 rT]%G. rewrite /= normal1 subG1 nt /=. apply/subsetP=> a Da; rewrite !inE Da /= sub1set !inE. by rewrite /= -actmE // morph1 eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)