{G : Group} (H : Subgroup G) : Group. Proof. apply (Build_Group (sig H) (fun '(x ; p) '(y ; q) => (x * y ; issubgroup_in_op x y p q)) (mon_unit ; issubgroup_in_unit) (fun '(x ; p) => (- x ; issubgroup_in_inv _ p))). repeat split. 1: exact _. all: grp_auto. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.