fact: Definition in_cosetR_inverse {G : Group} {N : NormalSubgroup G} : forall x y : G, in_cosetR N (-x) (-y) <~> in_cosetR N x y.
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType