{G : Group} {N : Subgroup G} : forall x y, in_cosetL N (-x * y) mon_unit <~> in_cosetL N x y. Proof. intros x y; cbn. rewrite (right_identity (- _)). rewrite (negate_sg_op _). rewrite (negate_involutive _). apply equiv_iff_hprop; apply symmetric_in_cosetL. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.