proposition: Lemma simple_compsP G s : comps G s -> reflect (s = [:: 1%G]) (simple G).
proof: Proof. move=> cs; apply: (iffP idP) => [|s1]; last first. by rewrite s1 /comps eqxx /= andbT -simple_maxnormal in cs. case: s cs => [/trivg_comps/eqP-> | H s]; first by case/simpleP; rewrite eqxx. rewrite [comps _ _]andbCA /= => /andP[/maxgroupp maxH /trivg_comps/esym nil_s]. rewrite simple_maxnormal => /maxgroupP[_ simG]. have H1: H = 1%G by apply/val_inj/simG; rewrite // sub1G. by move: nil_s; rewrite H1 eqxx => /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)