diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 060a8cb0a..79dd40e1e 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -20,41 +20,45 @@ namespace binary
     local notation a ⁻¹  := inv a
     local notation 1     := one
 
-    definition commutative := ∀a b, a * b = b * a
-    definition associative := ∀a b c, (a * b) * c = a * (b * c)
-    definition left_identity := ∀a, 1 * a = a
-    definition right_identity := ∀a, a * 1 = a
-    definition left_inverse := ∀a, a⁻¹ * a = 1
-    definition right_inverse := ∀a, a * a⁻¹ = 1
-    definition left_cancelative := ∀a b c, a * b = a * c → b = c
-    definition right_cancelative := ∀a b c, a * b = c * b → a = c
+    definition commutative [reducible] := ∀a b, a * b = b * a
+    definition associative [reducible] := ∀a b c, (a * b) * c = a * (b * c)
+    definition left_identity [reducible] := ∀a, 1 * a = a
+    definition right_identity [reducible] := ∀a, a * 1 = a
+    definition left_inverse [reducible] := ∀a, a⁻¹ * a = 1
+    definition right_inverse [reducible] := ∀a, a * a⁻¹ = 1
+    definition left_cancelative [reducible] := ∀a b c, a * b = a * c → b = c
+    definition right_cancelative [reducible] := ∀a b c, a * b = c * b → a = c
 
-    definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b
-    definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b
-    definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b =  a
-    definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a
+    definition inv_op_cancel_left [reducible] := ∀a b, a⁻¹ * (a * b) = b
+    definition op_inv_cancel_left [reducible] := ∀a b, a * (a⁻¹ * b) = b
+    definition inv_op_cancel_right [reducible] := ∀a b, a * b⁻¹ * b =  a
+    definition op_inv_cancel_right [reducible] := ∀a b, a * b * b⁻¹ = a
 
     variable (op₂ : A → A → A)
 
     local notation a + b := op₂ a b
 
-    definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
-    definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
+    definition left_distributive [reducible] := ∀a b c, a * (b + c) = a * b + a * c
+    definition right_distributive [reducible] := ∀a b c, (a + b) * c = a * c + b * c
+
+    definition right_commutative [reducible] {B : Type} (f : B → A → B) := ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
+    definition left_commutative [reducible] {B : Type}  (f : A → B → B) := ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
   end
 
+
   context
     variable {A : Type}
     variable {f : A → A → A}
     variable H_comm : commutative f
     variable H_assoc : associative f
     infixl `*` := f
-    theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
+    theorem left_comm : left_commutative f :=
     take a b c, calc
       a*(b*c) = (a*b)*c  : H_assoc
         ...   = (b*a)*c  : H_comm
         ...   = b*(a*c)  : H_assoc
 
-    theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
+    theorem right_comm : right_commutative f :=
     take a b c, calc
       (a*b)*c = a*(b*c) : H_assoc
         ...   = a*(c*b) : H_comm
diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 7e9ff6cd9..3d1b8664e 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -14,6 +14,12 @@ variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
 definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
 λx, f (g x)
 
+definition compose_right [reducible] (f : B → B → B) (g : A → B) : B → A → B :=
+λ b a, f b (g a)
+
+definition compose_left [reducible] (f : B → B → B) (g : A → B) : A → B → B :=
+λ a b, f (g a) b
+
 definition id [reducible] (a : A) : A :=
 a
 
diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean
index ac4e114d9..43e210505 100644
--- a/library/data/list/perm.lean
+++ b/library/data/list/perm.lean
@@ -467,27 +467,27 @@ assume p : l₁++(a::l₂) ~ l₃++(a::l₄),
 
 section foldl
   variables {f : B → A → B} {l₁ l₂ : list A}
-  variable rcomm : ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
+  variable rcomm : right_commutative f
   include  rcomm
 
-  theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ a, foldl f a l₁ = foldl f a l₂ :=
+  theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ b, foldl f b l₁ = foldl f b l₂ :=
   assume p, perm_induction_on p
-    (λ a, by rewrite *foldl_nil)
-    (λ x t₁ t₂ p r a, calc
-       foldl f a (x::t₁) = foldl f (f a x) t₁ : foldl_cons
-               ...       = foldl f (f a x) t₂ : r (f a x)
-               ...       = foldl f a (x::t₂)  : foldl_cons)
-    (λ x y t₁ t₂ p r a, calc
-       foldl f a (y :: x :: t₁) = foldl f (f (f a y) x) t₁ : by rewrite foldl_cons
-                     ...        = foldl f (f (f a x) y) t₁ : by rewrite rcomm
-                     ...        = foldl f (f (f a x) y) t₂ : r (f (f a x) y)
-                     ...        = foldl f a (x :: y :: t₂) : by rewrite foldl_cons)
-    (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
+    (λ b, by rewrite *foldl_nil)
+    (λ x t₁ t₂ p r b, calc
+       foldl f b (x::t₁) = foldl f (f b x) t₁ : foldl_cons
+               ...       = foldl f (f b x) t₂ : r (f b x)
+               ...       = foldl f b (x::t₂)  : foldl_cons)
+    (λ x y t₁ t₂ p r b, calc
+       foldl f b (y :: x :: t₁) = foldl f (f (f b y) x) t₁ : by rewrite foldl_cons
+                     ...        = foldl f (f (f b x) y) t₁ : by rewrite rcomm
+                     ...        = foldl f (f (f b x) y) t₂ : r (f (f b x) y)
+                     ...        = foldl f b (x :: y :: t₂) : by rewrite foldl_cons)
+    (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ b, eq.trans (r₁ b) (r₂ b))
 end foldl
 
 section foldr
   variables {f : A → B → B} {l₁ l₂ : list A}
-  variable lcomm : ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
+  variable lcomm : left_commutative f
   include  lcomm
 
   theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ b, foldr f b l₁ = foldr f b l₂ :=