From c7795905174a6f0800d71b311723f55f6b34115c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 30 Jan 2016 16:34:59 -0800
Subject: [PATCH] feat(library/algebra/ring): add lemma

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

diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 03b26299d..e5a912ce2 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -272,6 +272,10 @@ section
   theorem mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
   by simp
 
+  theorem add_mul_self_eq : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
+  calc (a + b)*(a + b) = a*a + (1+1)*a*b + b*b : by simp
+               ...     = a*a + 2*a*b + b*b     : by rewrite one_add_one_eq_two
+
   theorem dvd_neg_iff_dvd : (a ∣ -b) ↔ (a ∣ b) :=
   iff.intro
     (suppose a ∣ -b,