(x y : G) : H (x * y) -> H x -> H y. Proof. intros p q. rewrite <- (grp_unit_l y). revert q p. rewrite <- (grp_inv_l x). rewrite <- grp_assoc. apply issubgroup_in_inv_op. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.