AbGroup. Proof. rapply (Build_AbGroup grp_trivial). by intros []. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.