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