diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 63d615ad8a..b2c764ae06 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -541,6 +541,21 @@ Proof.
     apply path_contr.
 Defined.
 
+(** A maximal subgroup of a group [G] is a subgroup where every element of [G] is included. *)
+Class IsMaximalSubgroup {G : Group} (H : Subgroup G) :=
+  ismaximalsubgroup : forall (x : G), H x.
+
+Global Instance ishprop_ismaximalsubgroup `{Funext}
+  {G : Group} (H : Subgroup G)
+  : IsHProp (IsMaximalSubgroup H)
+  := istrunc_forall.
+
+Global Instance ismaximalsubgroup_maximalsubgroup {G : Group}
+  : IsMaximalSubgroup (maximal_subgroup G)
+  := fun g => tt.
+
+(** Note that we don't have an analogue for [istrivial_iff_grp_iso_trivial_group] since a proper subgroup of a group may be isomorphic to the entire group, whilst still being different from the maximal subgroup. The example to keep in mind is the group of integers [Z] and the subgroup of even integers [2Z]. Clearly, the integers are isomorphic to the even integers as groups, however the even integers are not equal to the maximal subgroup. *) 
+
 (** Intersection of two subgroups *)
 Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.
 Proof.