AbGroup. Proof. snrapply Build_AbGroup. 1: snrapply Build_Group. 5: repeat split. - exact (Vector A n). - exact vector_plus. - exact vector_zero. - exact vector_neg. - exact _. - exact associative_vector_plus. - exact left_identity_vector_plus. - exact right_identity_vector_plus. - exact left_inverse_vector_plus. - exact right_inverse_vector_plus. - exact commutative_vector_plus. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids. Require Import Types.Sigma. Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module. Require Import Spaces.Nat.Core. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import abstract_algebra.