From a23c05549ed8201a9e67e12f04b9214729a7a191 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 Oct 2015 15:04:01 -0700
Subject: [PATCH] fix(library/data/int/div): int div

---
 library/data/int/div.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 3208927b8..91fc6bf92 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -52,8 +52,6 @@ rfl
 
 notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
 
-lemma modulo.def (a b : ℤ) : a mod b = a - a div b * b := rfl
-
 /- div  -/
 
 theorem of_nat_div (m n : nat) : of_nat (m div n) = (of_nat m) div (of_nat n) :=