{G : Group} (N : NormalSubgroup G) {x y : G} : N x -> N (y * x * -y). Proof. intros n. apply isnormal. nrefine (transport N (grp_assoc _ _ _)^ _). nrefine (transport (fun y => N (y * x)) (grp_inv_l _)^ _). nrefine (transport N (grp_unit_l _)^ _). exact n. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.