proposition: Lemma simpleP gT (G : {group gT}) : reflect (G :!=: 1 /\ forall H : {group gT}, H <| G -> H :=: 1 \/ H :=: G) (simple G).
proof: Proof. apply: (iffP mingroupP); rewrite normG andbT => [[ntG simG]]. split=> // N /andP[sNG nNG]. by case: (eqsVneq N 1) => [|ntN]; [left | right; apply: simG; rewrite ?ntN]. split=> // N /andP[ntN nNG] sNG. by case: (simG N) ntN => // [|->]; [apply/andP | case/eqP]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)