{A : AbGroup} (x y : A) : - (x + y) = -x - y. Proof. lhs nrapply grp_inv_op. apply ab_comm. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.