{G : Group} (N : NormalSubgroup G) (x y : G) : in_cosetL N x y <~> in_cosetR N x y := equiv_in_cosetR_symm _ _ oE equiv_symmetric_in_normalsubgroup _ _ _.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.