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

Stream: general

[Reid Barton]

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]

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
  rw ← sub_add,
end

[Scott Morrison]

You know about abel?

[Chris Wong]

... I did not. Thanks for the suggestion :laughing: