diff --git a/library/data/prod.lean b/library/data/prod.lean
index f43ff7e62b..c82a0018bc 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -27,4 +27,15 @@ 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₃)
+
+  definition swap {A : Type} : A × A → A × A
+  | (a, b) := (b, a)
+
+  theorem swap_swap {A : Type} : ∀ p : A × A, swap (swap p) = p
+  | (a, b) := rfl
+
+  theorem eq_of_swap_eq {A : Type} : ∀ p₁ p₂ : A × A, swap p₁ = swap p₂ → p₁ = p₂ :=
+  take p₁ p₂, assume seqs,
+  assert h₁ : swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
+  by rewrite *swap_swap at h₁; exact h₁
 end prod