{G : Group} {N : NormalSubgroup G} (x y : G) : in_cosetR N (-x) (-y) <~> in_cosetR N x y. Proof. refine (_ oE equiv_in_cosetL_in_cosetR_normalsubgroup _ _ _); cbn. by rewrite grp_inv_inv. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.