diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 595e98827..4a058d7d3 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -326,7 +326,7 @@ or.elim (cases_of_nat_succ a)
 
 /- addition -/
 
-definition padd (p q : ℕ × ℕ) : ℕ × ℕ := map_pair2 nat.add p q
+definition padd (p q : ℕ × ℕ) : ℕ × ℕ := (pr1 p + pr1 q, pr2 p + pr2 q)
 
 theorem repr_add (a b : ℤ) :  repr (add a b) ≡ padd (repr a) (repr b) :=
 cases_on a
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 340bfdc80..2610fc05a 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -28,86 +28,4 @@ namespace prod
         (assume H, H ▸ and.intro rfl rfl)
         (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)),
     decidable_of_decidable_of_iff _ (iff.symm H₃)
-
-  -- ### flip operation
-
-  definition flip (a : A × B) : B × A := pair (pr2 a) (pr1 a)
-
-  theorem flip_def (a : A × B) : flip a = pair (pr2 a) (pr1 a) := rfl
-  theorem flip_pair (a : A) (b : B) : flip (pair a b) = pair b a := rfl
-  theorem flip_pr1 (a : A × B) : pr1 (flip a) = pr2 a := rfl
-  theorem flip_pr2 (a : A × B) : pr2 (flip a) = pr1 a := rfl
-  theorem flip_flip (a : A × B) : flip (flip a) = a :=
-  destruct a (take x y, rfl)
-
-  theorem P_flip {P : A → B → Prop} (a : A × B) (H : P (pr1 a) (pr2 a))
-    : P (pr2 (flip a)) (pr1 (flip a)) :=
-  (flip_pr1 a)⁻¹ ▸ (flip_pr2 a)⁻¹ ▸ H
-
-  theorem flip_inj {a b : A × B} (H : flip a = flip b) : a = b :=
-  have H2 : flip (flip a) = flip (flip b), from congr_arg flip H,
-  show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
-
-  -- ### coordinatewise unary maps
-
-  definition map_pair (f : A → B) (a : A × A) : B × B :=
-  pair (f (pr1 a)) (f (pr2 a))
-
-  theorem map_pair_def (f : A → B) (a : A × A)
-    : map_pair f a = pair (f (pr1 a)) (f (pr2 a)) :=
-  rfl
-
-  theorem map_pair_pair (f : A → B) (a a' : A)
-    : map_pair f (pair a a') = pair (f a) (f a') :=
-  (pr1.mk a a') ▸ (pr2.mk a a') ▸ rfl
-
-  theorem map_pair_pr1 (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
-  !pr1.mk
-
-  theorem map_pair_pr2 (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
-  !pr2.mk
-
-  -- ### coordinatewise binary maps
-
-  definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C :=
-  pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
-
-  theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-    map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
-
-  theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) :
-    map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
-  calc
-    map_pair2 f (pair a a') (pair b b')
-          = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
-              : {pr1.mk b b'}
-      ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.mk b b'}
-      ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.mk a a'}
-      ... = pair (f a b) (f a' b') : {pr1.mk a a'}
-
-  theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-  pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.mk
-
-  theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-  pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.mk
-
-  theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
-    flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
-  have Hx : pr1 (flip (map_pair2 f a b)) =  pr1 (map_pair2 f (flip a) (flip b)), from
-    calc
-      pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
-        ... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
-        ... = f (pr1 (flip a)) (pr2 b) : {(flip_pr1 a)⁻¹}
-        ... = f (pr1 (flip a)) (pr1 (flip b)) : {(flip_pr1 b)⁻¹}
-        ... = pr1 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr1 f _ _)⁻¹,
-  have Hy : pr2 (flip (map_pair2 f a b)) =  pr2 (map_pair2 f (flip a) (flip b)), from
-    calc
-      pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
-        ... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
-        ... = f (pr2 (flip a)) (pr1 b) : {flip_pr2 a}
-        ... = f (pr2 (flip a)) (pr2 (flip b)) : {flip_pr2 b}
-        ... = pr2 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr2 f _ _)⁻¹,
-  pair_eq Hx Hy
-
-
 end prod
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index dbf8701e5..f2d6ef3d6 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -1,6 +1,10 @@
--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.quotient.util
+Author: Floris van Doorn
+-/
 
 import logic ..prod algebra.relation
 import tools.fake_simplifier
@@ -10,8 +14,89 @@ open fake_simplifier
 
 namespace quotient
 
--- auxliary facts about products
--- -----------------------------
+/- auxiliary facts about products -/
+
+  variables {A B : Type}
+
+  /- flip -/
+
+  definition flip (a : A × B) : B × A := pair (pr2 a) (pr1 a)
+
+  theorem flip_def (a : A × B) : flip a = pair (pr2 a) (pr1 a) := rfl
+  theorem flip_pair (a : A) (b : B) : flip (pair a b) = pair b a := rfl
+  theorem flip_pr1 (a : A × B) : pr1 (flip a) = pr2 a := rfl
+  theorem flip_pr2 (a : A × B) : pr2 (flip a) = pr1 a := rfl
+  theorem flip_flip (a : A × B) : flip (flip a) = a :=
+  destruct a (take x y, rfl)
+
+  theorem P_flip {P : A → B → Prop} (a : A × B) (H : P (pr1 a) (pr2 a))
+    : P (pr2 (flip a)) (pr1 (flip a)) :=
+  (flip_pr1 a)⁻¹ ▸ (flip_pr2 a)⁻¹ ▸ H
+
+  theorem flip_inj {a b : A × B} (H : flip a = flip b) : a = b :=
+  have H2 : flip (flip a) = flip (flip b), from congr_arg flip H,
+  show a = b, from (flip_flip a) ▸ (flip_flip b) ▸ H2
+
+  /- coordinatewise unary maps -/
+
+  definition map_pair (f : A → B) (a : A × A) : B × B :=
+  pair (f (pr1 a)) (f (pr2 a))
+
+  theorem map_pair_def (f : A → B) (a : A × A)
+    : map_pair f a = pair (f (pr1 a)) (f (pr2 a)) :=
+  rfl
+
+  theorem map_pair_pair (f : A → B) (a a' : A)
+    : map_pair f (pair a a') = pair (f a) (f a') :=
+  (pr1.mk a a') ▸ (pr2.mk a a') ▸ rfl
+
+  theorem map_pair_pr1 (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) :=
+  !pr1.mk
+
+  theorem map_pair_pr2 (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) :=
+  !pr2.mk
+
+  /- coordinatewise binary maps -/
+
+  definition map_pair2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : C × C :=
+  pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b))
+
+  theorem map_pair2_def {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+    map_pair2 f a b = pair (f (pr1 a) (pr1 b)) (f (pr2 a) (pr2 b)) := rfl
+
+  theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) :
+    map_pair2 f (pair a a') (pair b b') = pair (f a b) (f a' b') :=
+  calc
+    map_pair2 f (pair a a') (pair b b')
+          = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b')))
+              : {pr1.mk b b'}
+      ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.mk b b'}
+      ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.mk a a'}
+      ... = pair (f a b) (f a' b') : {pr1.mk a a'}
+
+  theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+  pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.mk
+
+  theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+  pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.mk
+
+  theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) :
+    flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) :=
+  have Hx : pr1 (flip (map_pair2 f a b)) =  pr1 (map_pair2 f (flip a) (flip b)), from
+    calc
+      pr1 (flip (map_pair2 f a b)) = pr2 (map_pair2 f a b) : flip_pr1 _
+        ... = f (pr2 a) (pr2 b) : map_pair2_pr2 f a b
+        ... = f (pr1 (flip a)) (pr2 b) : {(flip_pr1 a)⁻¹}
+        ... = f (pr1 (flip a)) (pr1 (flip b)) : {(flip_pr1 b)⁻¹}
+        ... = pr1 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr1 f _ _)⁻¹,
+  have Hy : pr2 (flip (map_pair2 f a b)) =  pr2 (map_pair2 f (flip a) (flip b)), from
+    calc
+      pr2 (flip (map_pair2 f a b)) = pr1 (map_pair2 f a b) : flip_pr2 _
+        ... = f (pr1 a) (pr1 b) : map_pair2_pr1 f a b
+        ... = f (pr2 (flip a)) (pr1 b) : {flip_pr2 a}
+        ... = f (pr2 (flip a)) (pr2 (flip b)) : {flip_pr2 b}
+        ... = pr2 (map_pair2 f (flip a) (flip b)) : (map_pair2_pr2 f _ _)⁻¹,
+  pair_eq Hx Hy
 
 -- add_rewrite flip_pr1 flip_pr2 flip_pair
 -- add_rewrite map_pair_pr1 map_pair_pr2 map_pair_pair