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