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