(x y : G) : H x -> H y -> H (x * -y). Proof. intros p q. apply issubgroup_in_op. 1: assumption. by apply issubgroup_in_inv. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.