{A : AbGroup} (x y : A) : x + y = y + x := commutativity x y.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.