Build_IsNormalSubgroup' (G : Group) (N : Subgroup G) (isnormal : forall x y, N x -> N (y * x * -y)) : IsNormalSubgroup N. Proof. intros x y n. nrefine (transport N (grp_unit_r _) _). nrefine (transport (fun z => N (_ * z)) (grp_inv_r y) _). nrefine (transport N (grp_assoc _ _ _)^ _). nrefine (transport (fun z => N (z * _)) (grp_assoc _ _ _) _). by apply isnormal. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.