## Stream: general

### Topic: alternating_sum lemmas (was: Canonical form for "n is even")

#### Reid Barton (Aug 22 2020 at 09:33):

I would guess that simp will already simplify x - (y - z) to x - y + z, so there's no need for _cons_cons'

#### Chris Wong (Aug 22 2020 at 10:04):

You'd think so, but I've been surprised by how little simp does for add_comm_group. Here, simp fails, and library_search suggests sub_add reversed:

import algebra.group.basic

example {G : Type*} [add_comm_group G] (x y z : G) : x - (y - z) = x - y + z :=
begin

You know about abel?