{G : Group} (N : NormalSubgroup G) : forall x y, N (x * y) <~> N (y * x). Proof. intros x y. rapply equiv_iff_hprop. all: apply isnormal. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.