{G : Group} {N : Subgroup G} : forall x y, in_cosetL N x y <~> in_cosetL N y x. Proof. intros x y. srapply equiv_iff_hprop. all: by intro. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.