{G : Group} {N : Subgroup G} : forall x y, in_cosetR N (x * -y) mon_unit <~> in_cosetR N x y. Proof. intros x y; cbn. rewrite negate_mon_unit. rewrite (right_identity (x * -y)). reflexivity. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.