abgroup_Z@{} : AbGroup@{Set}. Proof. snrapply Build_AbGroup'. - exact Int. - exact 0. - exact int_neg. - exact int_add. - exact _. - exact int_add_comm. - exact int_add_assoc. - exact int_add_0_l. - exact int_add_neg_l. Defined.
Require Import Basics. Require Import Spaces.Pos.Core Spaces.Int. Require Import Algebra.AbGroups.AbelianGroup.