From 57bee2a6592e7fdc73a74e2c78d97368a203c8cb Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 8 Oct 2014 21:45:44 -0400
Subject: [PATCH] feat(binary.lean): add helper theorem for associative
 functions

---
 library/algebra/binary.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 5dfb4a8b60..8ac8236b91 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -31,4 +31,17 @@ namespace binary
         ...   = a*(c*b) : {H_comm}
         ...   = (a*c)*b : H_assoc⁻¹
   end
+
+  context
+    parameter {A : Type}
+    parameter {f : A → A → A}
+    hypothesis H_assoc : associative f
+    infixl `*`:75 := f
+    theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
+    calc
+      (a*b)*(c*d) = a*(b*(c*d)) : H_assoc
+              ... = a*((b*c)*d) : {H_assoc⁻¹}
+  end
+
+
 end binary