diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 0ebeb032cc..b5356e5bef 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -610,6 +610,12 @@ Proof.
   split; by apply subgroup_in_op_inv.
 Defined.
 
+(** *** Simple groups *)
+
+Class IsSimpleGroup (G : Group)
+  := is_simple_group : forall (N : Subgroup G) `{IsNormalSubgroup G N},
+    IsTrivialGroup N + IsMaximalSubgroup N.
+
 (** *** The subgroup generated by a subset *)
 
 (** Underlying type family of a subgroup generated by subset *)