QuotientGroup' (G : Group) (N : Subgroup G) (H : IsNormalSubgroup N) := QuotientGroup G (Build_NormalSubgroup G N H).
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import HSet. Require Import Spaces.Finite.Finite. Require Import WildCat. Require Import Modalities.Modality.