(G : AbGroup) (H : Subgroup G) : AbGroup := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.