Relation G := fun x y => H (x * -y). Hint Extern 4 => progress unfold in_cosetL : typeclass_instances. Hint Extern 4 => progress unfold : typeclass_instances. Global Arguments in_cosetL /. Global Arguments /. Global Instance ishprop_in_cosetL : is_mere_relation G in_cosetL := _. Global Instance ishprop_in_cosetR : is_mere_relation G := _. Global Instance reflexive_in_cosetL : Reflexive in_cosetL. Proof. intro x; hnf. rewrite left_inverse. apply issubgroup_in_unit. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.