From 1693932c9f3f80d15ad69033fca0ce7011cd7f69 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Fri, 31 Jul 2015 10:54:06 -0400
Subject: [PATCH] feat(library/algebra/group): add theorem to comm group

---
 library/algebra/group.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 9e68e68b9..a69341bbe 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -558,6 +558,10 @@ section add_comm_group
 
   theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c :=
   !add.comm ▸ add_eq_of_eq_sub H
+
+  theorem sub_sub_self (a b : A) : a - (a - b) = b :=
+  by rewrite [sub_eq_add_neg, neg_sub, add.comm, sub_add_cancel]
+ 
 end add_comm_group
 
 definition group_of_add_group (A : Type) [G : add_group A] : group A :=