diff --git a/library/standard/binary.lean b/library/standard/binary.lean
new file mode 100644
index 000000000..49979b7a2
--- /dev/null
+++ b/library/standard/binary.lean
@@ -0,0 +1,35 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import logic
+
+namespace binary
+section
+  parameter {A : Type}
+  parameter f : A → A → A
+  infixl `*`:75 := f
+
+  abbreviation commutative := ∀a b, a*b = b*a
+  abbreviation associative := ∀a b c, (a*b)*c = a*(b*c)
+end
+
+section
+  parameter {A : Type}
+  parameter {f : A → A → A}
+  infixl `*`:75 := f
+  hypothesis H_comm : commutative f
+  hypothesis H_assoc : associative f
+
+  theorem left_comm : ∀a b c, a*(b*c) = b*(a*c)
+  := take a b c, calc
+       a*(b*c) = (a*b)*c  : symm (H_assoc _ _ _)
+         ...   = (b*a)*c  : {H_comm _ _}
+         ...   = b*(a*c)  : H_assoc _ _ _
+
+  theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b
+  := take a b c, calc
+       (a*b)*c = a*(b*c) : H_assoc _ _ _
+         ...   = a*(c*b) : {H_comm _ _}
+         ...   = (a*c)*b : symm (H_assoc _ _ _)
+end
+end