sugroup_group of maximal_subgroup is iso to original group

Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: d6d33e40-310f-4066-bb9d-34775e41cbbd -->

theories/Algebra/Groups/Subgroup.v

@@ -222,6 +222,15 @@ Defined.
 Coercion maximal_subgroup : Group >-> Subgroup.
 Add Printing Coercion maximal_subgroup.
 
+(** The group inferred from the maximal subgroup is the original group. *)
+Definition grp_iso_subgroup_group_maximal (G : Group)
+  : subgroup_group (maximal_subgroup G) $<~> G.
+Proof.
+  snrapply Build_GroupIsomorphism'.
+  - rapply equiv_sigma_contr.
+  - hnf; reflexivity.
+Defined.
+
 (** Paths between subgroups correspond to homotopies between the underlying predicates. *) 
 Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G)
   : (H == K) <~> (H = K).