cleanup

src/Init/Data/Array/BinSearch.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Int.DivMod.Lemmas
 import Init.Omega
 universe u v
 

src/Init/Data/Int.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Data.Int.Basic
 import Init.Data.Int.Bitwise
 import Init.Data.Int.DivMod
-import Init.Data.Int.DivModLemmas
 import Init.Data.Int.Gcd
 import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Siddharth Bhat, Jeremy Avigad
 prelude
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Int.Bitwise
+import Init.Data.Int.DivMod.Lemmas
 
 namespace Int
 

src/Init/Data/Int/Cooper.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 prelude
-import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivMod.Lemmas
 import Init.Data.Int.Gcd
 
 /-!

src/Init/Data/Int/DivMod.lean

@@ -1,335 +1,9 @@
 /-
-Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Mario Carneiro
+Authors: Kim Morrison
 -/
 prelude
-import Init.Data.Int.Basic
-
-open Nat
-
-namespace Int
-
-/-! ## Quotient and remainder
-
-There are three main conventions for integer division,
-referred here as the E, F, T rounding conventions.
-All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
-and satisfy `x / 0 = 0` and `x % 0 = x`.
-
-### Historical notes
-In early versions of Lean, the typeclasses provided by `/` and `%`
-were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
-
-However we decided it was better to use `ediv` and `emod`,
-as they are consistent with the conventions used in SMTLib, and Mathlib,
-and often mathematical reasoning is easier with these conventions.
-
-At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
-In September 2024, we decided to do this rename (with deprecations in place),
-and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
-ever need to use these functions and their associated lemmas.
-
-In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
--/
-
-/-! ### E-rounding division
-This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
--/
-
-/--
-Integer division. This version of `Int.div` uses the E-rounding convention
-(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
-and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-
-This is the function powering the `/` notation on integers.
-
-Examples:
-```
-#eval (7 : Int) / (0 : Int) -- 0
-#eval (0 : Int) / (7 : Int) -- 0
-
-#eval (12 : Int) / (6 : Int) -- 2
-#eval (12 : Int) / (-6 : Int) -- -2
-#eval (-12 : Int) / (6 : Int) -- -2
-#eval (-12 : Int) / (-6 : Int) -- 2
-
-#eval (12 : Int) / (7 : Int) -- 1
-#eval (12 : Int) / (-7 : Int) -- -1
-#eval (-12 : Int) / (7 : Int) -- -2
-#eval (-12 : Int) / (-7 : Int) -- 2
-```
-
-Implemented by efficient native code.
--/
-@[extern "lean_int_ediv"]
-def ediv : (@& Int) → (@& Int) → Int
-  | ofNat m, ofNat n => ofNat (m / n)
-  | ofNat m, -[n+1]  => -ofNat (m / succ n)
-  | -[_+1],  0       => 0
-  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
-  | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
-
-/--
-Integer modulus. This version of `Int.mod` uses the E-rounding convention
-(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
-and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-
-This is the function powering the `%` notation on integers.
-
-Examples:
-```
-#eval (7 : Int) % (0 : Int) -- 7
-#eval (0 : Int) % (7 : Int) -- 0
-
-#eval (12 : Int) % (6 : Int) -- 0
-#eval (12 : Int) % (-6 : Int) -- 0
-#eval (-12 : Int) % (6 : Int) -- 0
-#eval (-12 : Int) % (-6 : Int) -- 0
-
-#eval (12 : Int) % (7 : Int) -- 5
-#eval (12 : Int) % (-7 : Int) -- 5
-#eval (-12 : Int) % (7 : Int) -- 2
-#eval (-12 : Int) % (-7 : Int) -- 2
-```
-
-Implemented by efficient native code.
--/
-@[extern "lean_int_emod"]
-def emod : (@& Int) → (@& Int) → Int
-  | ofNat m, n => ofNat (m % natAbs n)
-  | -[m+1],  n => subNatNat (natAbs n) (succ (m % natAbs n))
-
-/--
-The Div and Mod syntax uses ediv and emod for compatibility with SMTLIb and mathematical
-reasoning tends to be easier.
--/
-instance : Div Int where
-  div := Int.ediv
-instance : Mod Int where
-  mod := Int.emod
-
-@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
-
-theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
-theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / ↑(b+1) : Int) = -[a / succ b +1] := rfl
-theorem negSucc_ediv_negSucc {a b : Nat} : ((-[a+1]) / (-[b+1]) : Int) = ((a / (b + 1)) + 1 : Nat) := rfl
-
-theorem negSucc_emod_ofNat {a b : Nat} : -[a+1] % (b : Int) = subNatNat b (succ (a % b)) := rfl
-theorem negSucc_emod_negSucc {a b : Nat} : -[a+1] % -[b+1] = subNatNat (b + 1) (succ (a % (b + 1))) := rfl
-
-/-! ### T-rounding division -/
-
-/--
-`tdiv` uses the [*"T-rounding"*][t-rounding]
-(**T**runcation-rounding) convention, meaning that it rounds toward
-zero. Also note that division by zero is defined to equal zero.
-
-  The relation between integer division and modulo is found in
-  `Int.tmod_add_tdiv` which states that
-  `tmod a b + b * (tdiv a b) = a`, unconditionally.
-
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
-
-  Examples:
-
-  ```
-  #eval (7 : Int).tdiv (0 : Int) -- 0
-  #eval (0 : Int).tdiv (7 : Int) -- 0
-
-  #eval (12 : Int).tdiv (6 : Int) -- 2
-  #eval (12 : Int).tdiv (-6 : Int) -- -2
-  #eval (-12 : Int).tdiv (6 : Int) -- -2
-  #eval (-12 : Int).tdiv (-6 : Int) -- 2
-
-  #eval (12 : Int).tdiv (7 : Int) -- 1
-  #eval (12 : Int).tdiv (-7 : Int) -- -1
-  #eval (-12 : Int).tdiv (7 : Int) -- -1
-  #eval (-12 : Int).tdiv (-7 : Int) -- 1
-  ```
-
-  Implemented by efficient native code.
--/
-@[extern "lean_int_div"]
-def tdiv : (@& Int) → (@& Int) → Int
-  | ofNat m, ofNat n =>  ofNat (m / n)
-  | ofNat m, -[n +1] => -ofNat (m / succ n)
-  | -[m +1], ofNat n => -ofNat (succ m / n)
-  | -[m +1], -[n +1] =>  ofNat (succ m / succ n)
-
-/-- Integer modulo. This function uses the
-  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
-  to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
-  unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
-  particular, `a % 0 = a`.
-
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
-
-  Examples:
-
-  ```
-  #eval (7 : Int).tmod (0 : Int) -- 7
-  #eval (0 : Int).tmod (7 : Int) -- 0
-
-  #eval (12 : Int).tmod (6 : Int) -- 0
-  #eval (12 : Int).tmod (-6 : Int) -- 0
-  #eval (-12 : Int).tmod (6 : Int) -- 0
-  #eval (-12 : Int).tmod (-6 : Int) -- 0
-
-  #eval (12 : Int).tmod (7 : Int) -- 5
-  #eval (12 : Int).tmod (-7 : Int) -- 5
-  #eval (-12 : Int).tmod (7 : Int) -- -5
-  #eval (-12 : Int).tmod (-7 : Int) -- -5
-  ```
-
-  Implemented by efficient native code. -/
-@[extern "lean_int_mod"]
-def tmod : (@& Int) → (@& Int) → Int
-  | ofNat m, ofNat n =>  ofNat (m % n)
-  | ofNat m, -[n +1] =>  ofNat (m % succ n)
-  | -[m +1], ofNat n => -ofNat (succ m % n)
-  | -[m +1], -[n +1] => -ofNat (succ m % succ n)
-
-theorem ofNat_tdiv (m n : Nat) : ↑(m / n) = tdiv ↑m ↑n := rfl
-
-/-! ### F-rounding division
-This pair satisfies `fdiv x y = floor (x / y)`.
--/
-
-/--
-Integer division. This version of division uses the F-rounding convention
-(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
-and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-
-Examples:
-```
-#eval (7 : Int).fdiv (0 : Int) -- 0
-#eval (0 : Int).fdiv (7 : Int) -- 0
-
-#eval (12 : Int).fdiv (6 : Int) -- 2
-#eval (12 : Int).fdiv (-6 : Int) -- -2
-#eval (-12 : Int).fdiv (6 : Int) -- -2
-#eval (-12 : Int).fdiv (-6 : Int) -- 2
-
-#eval (12 : Int).fdiv (7 : Int) -- 1
-#eval (12 : Int).fdiv (-7 : Int) -- -2
-#eval (-12 : Int).fdiv (7 : Int) -- -2
-#eval (-12 : Int).fdiv (-7 : Int) -- 1
-```
--/
-def fdiv : Int → Int → Int
-  | 0,       _       => 0
-  | ofNat m, ofNat n => ofNat (m / n)
-  | ofNat (succ m), -[n+1] => -[m / succ n +1]
-  | -[_+1],  0       => 0
-  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
-  | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
-
-/--
-Integer modulus. This version of `Int.mod` uses the F-rounding convention
-(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
-and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-
-Examples:
-
-```
-#eval (7 : Int).fmod (0 : Int) -- 7
-#eval (0 : Int).fmod (7 : Int) -- 0
-
-#eval (12 : Int).fmod (6 : Int) -- 0
-#eval (12 : Int).fmod (-6 : Int) -- 0
-#eval (-12 : Int).fmod (6 : Int) -- 0
-#eval (-12 : Int).fmod (-6 : Int) -- 0
-
-#eval (12 : Int).fmod (7 : Int) -- 5
-#eval (12 : Int).fmod (-7 : Int) -- -2
-#eval (-12 : Int).fmod (7 : Int) -- 2
-#eval (-12 : Int).fmod (-7 : Int) -- -5
-```
--/
-def fmod : Int → Int → Int
-  | 0,       _       => 0
-  | ofNat m, ofNat n => ofNat (m % n)
-  | ofNat (succ m),  -[n+1]  => subNatNat (m % succ n) n
-  | -[m+1],  ofNat n => subNatNat n (succ (m % n))
-  | -[m+1],  -[n+1]  => -ofNat (succ m % succ n)
-
-theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
-  | 0, _ => by simp [fdiv]
-  | succ _, _ => rfl
-
-/-!
-# `bmod` ("balanced" mod)
-
-Balanced mod (and balanced div) are a division and modulus pair such
-that `b * (Int.bdiv a b) + Int.bmod a b = a` and
-`-b/2 ≤ Int.bmod a b < b/2` for all `a : Int` and `b > 0`.
-
-This is used in Omega as well as signed bitvectors.
--/
-
-/--
-Balanced modulus.  This version of Integer modulus uses the
-balanced rounding convention, which guarantees that
-`-m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
-to `x` modulo `m`.
-
-If `m = 0`, then `bmod x m = x`.
-
-Examples:
-```
-#eval (7 : Int).bdiv 0 -- 0
-#eval (0 : Int).bdiv 7 -- 0
-
-#eval (12 : Int).bdiv 6 -- 2
-#eval (12 : Int).bdiv 7 -- 2
-#eval (12 : Int).bdiv 8 -- 2
-#eval (12 : Int).bdiv 9 -- 1
-
-#eval (-12 : Int).bdiv 6 -- -2
-#eval (-12 : Int).bdiv 7 -- -2
-#eval (-12 : Int).bdiv 8 -- -1
-#eval (-12 : Int).bdiv 9 -- -1
-```
--/
-def bmod (x : Int) (m : Nat) : Int :=
-  let r := x % m
-  if r < (m + 1) / 2 then
-    r
-  else
-    r - m
-
-/--
-Balanced division.  This returns the unique integer so that
-`b * (Int.bdiv a b) + Int.bmod a b = a`.
-
-Examples:
-```
-#eval (7 : Int).bmod 0 -- 7
-#eval (0 : Int).bmod 7 -- 0
-
-#eval (12 : Int).bmod 6 -- 0
-#eval (12 : Int).bmod 7 -- -2
-#eval (12 : Int).bmod 8 -- -4
-#eval (12 : Int).bmod 9 -- 3
-
-#eval (-12 : Int).bmod 6 -- 0
-#eval (-12 : Int).bmod 7 -- 2
-#eval (-12 : Int).bmod 8 -- -4
-#eval (-12 : Int).bmod 9 -- -3
-```
--/
-def bdiv (x : Int) (m : Nat) : Int :=
-  if m = 0 then
-    0
-  else
-    let q := x / m
-    let r := x % m
-    if r < (m + 1) / 2 then
-      q
-    else
-      q + 1
-
-end Int
+import Init.Data.Int.DivMod.Basic
+import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas

src/Init/Data/Int/DivMod/Basic.lean

@@ -0,0 +1,335 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Basic
+
+open Nat
+
+namespace Int
+
+/-! ## Quotient and remainder
+
+There are three main conventions for integer division,
+referred here as the E, F, T rounding conventions.
+All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
+and satisfy `x / 0 = 0` and `x % 0 = x`.
+
+### Historical notes
+In early versions of Lean, the typeclasses provided by `/` and `%`
+were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
+
+However we decided it was better to use `ediv` and `emod`,
+as they are consistent with the conventions used in SMTLib, and Mathlib,
+and often mathematical reasoning is easier with these conventions.
+
+At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
+In September 2024, we decided to do this rename (with deprecations in place),
+and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
+ever need to use these functions and their associated lemmas.
+
+In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
+-/
+
+/-! ### E-rounding division
+This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
+-/
+
+/--
+Integer division. This version of `Int.div` uses the E-rounding convention
+(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
+and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
+
+This is the function powering the `/` notation on integers.
+
+Examples:
+```
+#eval (7 : Int) / (0 : Int) -- 0
+#eval (0 : Int) / (7 : Int) -- 0
+
+#eval (12 : Int) / (6 : Int) -- 2
+#eval (12 : Int) / (-6 : Int) -- -2
+#eval (-12 : Int) / (6 : Int) -- -2
+#eval (-12 : Int) / (-6 : Int) -- 2
+
+#eval (12 : Int) / (7 : Int) -- 1
+#eval (12 : Int) / (-7 : Int) -- -1
+#eval (-12 : Int) / (7 : Int) -- -2
+#eval (-12 : Int) / (-7 : Int) -- 2
+```
+
+Implemented by efficient native code.
+-/
+@[extern "lean_int_ediv"]
+def ediv : (@& Int) → (@& Int) → Int
+  | ofNat m, ofNat n => ofNat (m / n)
+  | ofNat m, -[n+1]  => -ofNat (m / succ n)
+  | -[_+1],  0       => 0
+  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
+  | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
+
+/--
+Integer modulus. This version of `Int.mod` uses the E-rounding convention
+(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
+and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
+
+This is the function powering the `%` notation on integers.
+
+Examples:
+```
+#eval (7 : Int) % (0 : Int) -- 7
+#eval (0 : Int) % (7 : Int) -- 0
+
+#eval (12 : Int) % (6 : Int) -- 0
+#eval (12 : Int) % (-6 : Int) -- 0
+#eval (-12 : Int) % (6 : Int) -- 0
+#eval (-12 : Int) % (-6 : Int) -- 0
+
+#eval (12 : Int) % (7 : Int) -- 5
+#eval (12 : Int) % (-7 : Int) -- 5
+#eval (-12 : Int) % (7 : Int) -- 2
+#eval (-12 : Int) % (-7 : Int) -- 2
+```
+
+Implemented by efficient native code.
+-/
+@[extern "lean_int_emod"]
+def emod : (@& Int) → (@& Int) → Int
+  | ofNat m, n => ofNat (m % natAbs n)
+  | -[m+1],  n => subNatNat (natAbs n) (succ (m % natAbs n))
+
+/--
+The Div and Mod syntax uses ediv and emod for compatibility with SMTLIb and mathematical
+reasoning tends to be easier.
+-/
+instance : Div Int where
+  div := Int.ediv
+instance : Mod Int where
+  mod := Int.emod
+
+@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+
+theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
+theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / ↑(b+1) : Int) = -[a / succ b +1] := rfl
+theorem negSucc_ediv_negSucc {a b : Nat} : ((-[a+1]) / (-[b+1]) : Int) = ((a / (b + 1)) + 1 : Nat) := rfl
+
+theorem negSucc_emod_ofNat {a b : Nat} : -[a+1] % (b : Int) = subNatNat b (succ (a % b)) := rfl
+theorem negSucc_emod_negSucc {a b : Nat} : -[a+1] % -[b+1] = subNatNat (b + 1) (succ (a % (b + 1))) := rfl
+
+/-! ### T-rounding division -/
+
+/--
+`tdiv` uses the [*"T-rounding"*][t-rounding]
+(**T**runcation-rounding) convention, meaning that it rounds toward
+zero. Also note that division by zero is defined to equal zero.
+
+  The relation between integer division and modulo is found in
+  `Int.tmod_add_tdiv` which states that
+  `tmod a b + b * (tdiv a b) = a`, unconditionally.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int).tdiv (0 : Int) -- 0
+  #eval (0 : Int).tdiv (7 : Int) -- 0
+
+  #eval (12 : Int).tdiv (6 : Int) -- 2
+  #eval (12 : Int).tdiv (-6 : Int) -- -2
+  #eval (-12 : Int).tdiv (6 : Int) -- -2
+  #eval (-12 : Int).tdiv (-6 : Int) -- 2
+
+  #eval (12 : Int).tdiv (7 : Int) -- 1
+  #eval (12 : Int).tdiv (-7 : Int) -- -1
+  #eval (-12 : Int).tdiv (7 : Int) -- -1
+  #eval (-12 : Int).tdiv (-7 : Int) -- 1
+  ```
+
+  Implemented by efficient native code.
+-/
+@[extern "lean_int_div"]
+def tdiv : (@& Int) → (@& Int) → Int
+  | ofNat m, ofNat n =>  ofNat (m / n)
+  | ofNat m, -[n +1] => -ofNat (m / succ n)
+  | -[m +1], ofNat n => -ofNat (succ m / n)
+  | -[m +1], -[n +1] =>  ofNat (succ m / succ n)
+
+/-- Integer modulo. This function uses the
+  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
+  to pair with `Int.tdiv`, meaning that `tmod a b + b * (tdiv a b) = a`
+  unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
+  particular, `a % 0 = a`.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int).tmod (0 : Int) -- 7
+  #eval (0 : Int).tmod (7 : Int) -- 0
+
+  #eval (12 : Int).tmod (6 : Int) -- 0
+  #eval (12 : Int).tmod (-6 : Int) -- 0
+  #eval (-12 : Int).tmod (6 : Int) -- 0
+  #eval (-12 : Int).tmod (-6 : Int) -- 0
+
+  #eval (12 : Int).tmod (7 : Int) -- 5
+  #eval (12 : Int).tmod (-7 : Int) -- 5
+  #eval (-12 : Int).tmod (7 : Int) -- -5
+  #eval (-12 : Int).tmod (-7 : Int) -- -5
+  ```
+
+  Implemented by efficient native code. -/
+@[extern "lean_int_mod"]
+def tmod : (@& Int) → (@& Int) → Int
+  | ofNat m, ofNat n =>  ofNat (m % n)
+  | ofNat m, -[n +1] =>  ofNat (m % succ n)
+  | -[m +1], ofNat n => -ofNat (succ m % n)
+  | -[m +1], -[n +1] => -ofNat (succ m % succ n)
+
+theorem ofNat_tdiv (m n : Nat) : ↑(m / n) = tdiv ↑m ↑n := rfl
+
+/-! ### F-rounding division
+This pair satisfies `fdiv x y = floor (x / y)`.
+-/
+
+/--
+Integer division. This version of division uses the F-rounding convention
+(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
+and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
+
+Examples:
+```
+#eval (7 : Int).fdiv (0 : Int) -- 0
+#eval (0 : Int).fdiv (7 : Int) -- 0
+
+#eval (12 : Int).fdiv (6 : Int) -- 2
+#eval (12 : Int).fdiv (-6 : Int) -- -2
+#eval (-12 : Int).fdiv (6 : Int) -- -2
+#eval (-12 : Int).fdiv (-6 : Int) -- 2
+
+#eval (12 : Int).fdiv (7 : Int) -- 1
+#eval (12 : Int).fdiv (-7 : Int) -- -2
+#eval (-12 : Int).fdiv (7 : Int) -- -2
+#eval (-12 : Int).fdiv (-7 : Int) -- 1
+```
+-/
+def fdiv : Int → Int → Int
+  | 0,       _       => 0
+  | ofNat m, ofNat n => ofNat (m / n)
+  | ofNat (succ m), -[n+1] => -[m / succ n +1]
+  | -[_+1],  0       => 0
+  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
+  | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
+
+/--
+Integer modulus. This version of `Int.mod` uses the F-rounding convention
+(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
+and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
+
+Examples:
+
+```
+#eval (7 : Int).fmod (0 : Int) -- 7
+#eval (0 : Int).fmod (7 : Int) -- 0
+
+#eval (12 : Int).fmod (6 : Int) -- 0
+#eval (12 : Int).fmod (-6 : Int) -- 0
+#eval (-12 : Int).fmod (6 : Int) -- 0
+#eval (-12 : Int).fmod (-6 : Int) -- 0
+
+#eval (12 : Int).fmod (7 : Int) -- 5
+#eval (12 : Int).fmod (-7 : Int) -- -2
+#eval (-12 : Int).fmod (7 : Int) -- 2
+#eval (-12 : Int).fmod (-7 : Int) -- -5
+```
+-/
+def fmod : Int → Int → Int
+  | 0,       _       => 0
+  | ofNat m, ofNat n => ofNat (m % n)
+  | ofNat (succ m),  -[n+1]  => subNatNat (m % succ n) n
+  | -[m+1],  ofNat n => subNatNat n (succ (m % n))
+  | -[m+1],  -[n+1]  => -ofNat (succ m % succ n)
+
+theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
+  | 0, _ => by simp [fdiv]
+  | succ _, _ => rfl
+
+/-!
+# `bmod` ("balanced" mod)
+
+Balanced mod (and balanced div) are a division and modulus pair such
+that `b * (Int.bdiv a b) + Int.bmod a b = a` and
+`-b/2 ≤ Int.bmod a b < b/2` for all `a : Int` and `b > 0`.
+
+This is used in Omega as well as signed bitvectors.
+-/
+
+/--
+Balanced modulus.  This version of Integer modulus uses the
+balanced rounding convention, which guarantees that
+`-m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
+to `x` modulo `m`.
+
+If `m = 0`, then `bmod x m = x`.
+
+Examples:
+```
+#eval (7 : Int).bdiv 0 -- 0
+#eval (0 : Int).bdiv 7 -- 0
+
+#eval (12 : Int).bdiv 6 -- 2
+#eval (12 : Int).bdiv 7 -- 2
+#eval (12 : Int).bdiv 8 -- 2
+#eval (12 : Int).bdiv 9 -- 1
+
+#eval (-12 : Int).bdiv 6 -- -2
+#eval (-12 : Int).bdiv 7 -- -2
+#eval (-12 : Int).bdiv 8 -- -1
+#eval (-12 : Int).bdiv 9 -- -1
+```
+-/
+def bmod (x : Int) (m : Nat) : Int :=
+  let r := x % m
+  if r < (m + 1) / 2 then
+    r
+  else
+    r - m
+
+/--
+Balanced division.  This returns the unique integer so that
+`b * (Int.bdiv a b) + Int.bmod a b = a`.
+
+Examples:
+```
+#eval (7 : Int).bmod 0 -- 7
+#eval (0 : Int).bmod 7 -- 0
+
+#eval (12 : Int).bmod 6 -- 0
+#eval (12 : Int).bmod 7 -- -2
+#eval (12 : Int).bmod 8 -- -4
+#eval (12 : Int).bmod 9 -- 3
+
+#eval (-12 : Int).bmod 6 -- 0
+#eval (-12 : Int).bmod 7 -- 2
+#eval (-12 : Int).bmod 8 -- -4
+#eval (-12 : Int).bmod 9 -- -3
+```
+-/
+def bdiv (x : Int) (m : Nat) : Int :=
+  if m = 0 then
+    0
+  else
+    let q := x / m
+    let r := x % m
+    if r < (m + 1) / 2 then
+      q
+    else
+      q + 1
+
+end Int

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -0,0 +1,316 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Mario Carneiro
+-/
+
+prelude
+import Init.Data.Int.DivMod.Basic
+import Init.Data.Int.Order
+import Init.Data.Nat.Dvd
+import Init.RCases
+
+/-!
+# Lemmas about integer division needed to bootstrap `omega`.
+-/
+
+open Nat (succ)
+
+namespace Int
+
+-- /-! ### dvd  -/
+
+protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
+
+@[simp] protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
+
+@[simp] protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
+
+@[simp] protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
+
+protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
+  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])
+
+@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
+  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
+  match Int.le_total a 0 with
+  | .inl h =>
+    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
+    rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
+    apply Nat.dvd_zero
+  | .inr h => match a, eq_ofNat_of_zero_le h with
+    | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
+
+@[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
+  Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
+            (fun h => h.symm ▸ Int.dvd_refl _)
+
+protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩
+
+protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm ..⟩
+
+@[simp] protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
+  constructor <;> exact fun ⟨k, e⟩ =>
+    ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
+
+protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
+  constructor <;> exact fun ⟨k, e⟩ =>
+    ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
+
+@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
+  refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
+  rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
+  cases hk <;> subst b
+  · apply Int.dvd_mul_right
+  · rw [← Int.mul_neg]; apply Int.dvd_mul_right
+
+theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
+  rw [← natAbs_dvd_natAbs, natAbs_ofNat]
+
+/-! ### *div zero  -/
+
+@[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
+  | ofNat _ => show ofNat _ = _ by simp
+  | -[_+1] => show -ofNat _ = _ by simp
+
+@[simp] protected theorem ediv_zero : ∀ a : Int, a / 0 = 0
+  | ofNat _ => show ofNat _ = _ by simp
+  | -[_+1] => rfl
+
+/-! ### mod zero -/
+
+@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
+
+@[simp] theorem emod_zero : ∀ a : Int, a % 0 = a
+  | ofNat _ => congrArg ofNat <| Nat.mod_zero _
+  | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
+
+/-! ### ofNat mod -/
+
+@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+
+
+/-! ### mod definitions -/
+
+theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
+  | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
+  | ofNat m, -[n+1] => by
+    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
+    rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
+  | -[_+1], 0 => by rw [emod_zero]; rfl
+  | -[m+1], succ n => aux m n.succ
+  | -[m+1], -[n+1] => aux m n.succ
+where
+  aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by
+    rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
+      ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
+    exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
+
+theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
+  rw [Int.mul_comm]; exact emod_add_ediv ..
+
+theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
+  rw [Int.add_comm]; exact emod_add_ediv ..
+
+theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
+  rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
+
+/-! ### `/` ediv -/
+
+@[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
+  | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
+  | ofNat _, -[_+1] => (Int.neg_neg _).symm
+  | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
+
+protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl
+
+theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b :=
+  suffices ∀ {{a b c : Int}}, 0 < c → (a + b * c).ediv c = a.ediv c + b from
+    match Int.lt_trichotomy c 0 with
+    | Or.inl hlt => by
+      rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]
+      exact this (Int.neg_pos_of_neg hlt)
+    | Or.inr (Or.inl HEq) => absurd HEq H
+    | Or.inr (Or.inr hgt) => this hgt
+  suffices ∀ {k n : Nat} {a : Int}, (a + n * k.succ).ediv k.succ = a.ediv k.succ + n from
+    fun a b c H => match c, eq_succ_of_zero_lt H, b with
+      | _, ⟨_, rfl⟩, ofNat _ => this
+      | _, ⟨k, rfl⟩, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
+        rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
+  fun {k n} => @fun
+  | ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
+  | -[m+1] => by
+    show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
+    by_cases h : m < n * k.succ
+    · rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
+      apply congrArg ofNat
+      rw [Nat.mul_comm, Nat.mul_sub_div]; rwa [Nat.mul_comm]
+    · have h := Nat.not_lt.1 h
+      have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
+        rw [negSucc_eq, Int.ofNat_sub h]
+        simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]
+      show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
+      rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
+      apply congrArg negSucc
+      rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
+
+theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
+  if h : c = 0 then by simp [h] else by
+    let ⟨k, hk⟩ := H
+    rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
+      ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
+
+theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
+  rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]
+
+@[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
+  have := Int.add_mul_ediv_right 0 a H
+  rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this
+
+@[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
+  Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
+
+theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0 := by
+  rw [Int.div_def]
+  match b, h with
+  | Int.ofNat (b+1), _ =>
+    rcases a with ⟨a⟩ <;> simp [Int.ediv]
+    norm_cast
+    simp
+
+/-! ### emod -/
+
+theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
+  | ofNat _, _, _ => ofNat_zero_le _
+  | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
+
+theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
+  match a, b, eq_succ_of_zero_lt H with
+  | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
+  | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
+
+theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
+  calc k * (x / k)
+    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
+    _ = x                   := ediv_add_emod _ _
+
+theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
+  calc x
+    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
+    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
+
+@[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
+  if cz : c = 0 then by
+    rw [cz, Int.mul_zero, Int.add_zero]
+  else by
+    rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
+      Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]
+
+@[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
+  rw [Int.mul_comm, Int.add_mul_emod_self]
+
+@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
+  have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
+  rwa [Int.add_right_comm, emod_add_ediv] at this
+
+@[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
+  rw [Int.add_comm, emod_add_emod, Int.add_comm]
+
+theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n := by
+  rw [add_emod_emod, emod_add_emod]
+
+theorem add_emod_eq_add_emod_right {m n k : Int} (i : Int)
+    (H : m % n = k % n) : (m + i) % n = (k + i) % n := by
+  rw [← emod_add_emod, ← emod_add_emod k, H]
+
+theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔ m % n = k % n :=
+  ⟨fun H => by
+    have := add_emod_eq_add_emod_right (-i) H
+    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
+  add_emod_eq_add_emod_right _⟩
+
+@[simp] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
+  rw [← Int.zero_add (a * b), Int.add_mul_emod_self, Int.zero_emod]
+
+@[simp] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
+  rw [Int.mul_comm, mul_emod_left]
+
+theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
+  conv => lhs; rw [
+    ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
+    Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
+    ← Int.mul_assoc, add_mul_emod_self]
+
+@[simp] theorem emod_self {a : Int} : a % a = 0 := by
+  have := mul_emod_left 1 a; rwa [Int.one_mul] at this
+
+@[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
+    (h : m ∣ k) : (n % k) % m = n % m := by
+  conv => rhs; rw [← emod_add_ediv n k]
+  match k, h with
+  | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
+
+@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
+  conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
+
+theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
+  apply (emod_add_cancel_right b).mp
+  rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]
+
+/-! ### properties of `/` and `%` -/
+
+theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
+  have := emod_add_ediv a b; rwa [H, Int.zero_add] at this
+
+theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
+  rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]
+
+theorem dvd_of_emod_eq_zero {a b : Int} (H : b % a = 0) : a ∣ b :=
+  ⟨b / a, (mul_ediv_cancel_of_emod_eq_zero H).symm⟩
+
+theorem emod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → b % a = 0
+  | _, _, ⟨_, rfl⟩ => mul_emod_right ..
+
+theorem dvd_iff_emod_eq_zero {a b : Int} : a ∣ b ↔ b % a = 0 :=
+  ⟨emod_eq_zero_of_dvd, dvd_of_emod_eq_zero⟩
+
+protected theorem mul_ediv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b) / c = a * (b / c)
+  | _, c, ⟨d, rfl⟩ =>
+    if cz : c = 0 then by simp [cz, Int.mul_zero] else by
+      rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]
+
+protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
+    (h : c ∣ a) : (a * b) / c = a / c * b := by
+  rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]
+
+theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
+  | _, b, ⟨c, rfl⟩ => by
+    by_cases bz : b = 0
+    · simp [bz]
+    · rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
+
+theorem sub_ediv_of_dvd (a : Int) {b c : Int}
+    (hcb : c ∣ b) : (a - b) / c = a / c - b / c := by
+  rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
+  congr; exact Int.neg_ediv_of_dvd hcb
+
+protected theorem ediv_mul_cancel {a b : Int} (H : b ∣ a) : a / b * b = a :=
+  ediv_mul_cancel_of_emod_eq_zero (emod_eq_zero_of_dvd H)
+
+protected theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b := by
+  rw [Int.mul_comm, Int.ediv_mul_cancel H]
+
+/-! ### bmod -/
+
+@[simp] theorem bmod_emod : bmod x m % m = x % m := by
+  dsimp [bmod]
+  split <;> simp [Int.sub_emod]
+
+theorem bmod_def (x : Int) (m : Nat) : bmod x m =
+  if (x % m) < (m + 1) / 2 then
+    x % m
+  else
+    (x % m) - m :=
+  rfl
+
+end Int

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -5,13 +5,15 @@ Authors: Jeremy Avigad, Mario Carneiro
 -/
 
 prelude
-import Init.Data.Int.DivMod
+import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Nat.Lemmas
 import Init.Data.Int.Order
+import Init.Data.Int.Lemmas
 import Init.Data.Nat.Dvd
 import Init.RCases
 
 /-!
-# Lemmas about integer division needed to bootstrap `omega`.
+# Further lemmas about integer division, now that `omega` is available.
 -/
 
 open Nat (succ)
@@ -20,58 +22,11 @@ namespace Int
 
 /-! ### dvd  -/
 
-protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
-
-@[simp] protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
-
-@[simp] protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
-
-@[simp] protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
-
-protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
-  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])
-
-@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
-  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
-  match Int.le_total a 0 with
-  | .inl h =>
-    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
-    rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
-    apply Nat.dvd_zero
-  | .inr h => match a, eq_ofNat_of_zero_le h with
-    | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
-
 theorem dvd_antisymm {a b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b := by
   rw [← natAbs_of_nonneg H1, ← natAbs_of_nonneg H2]
   rw [ofNat_dvd, ofNat_dvd, ofNat_inj]
   apply Nat.dvd_antisymm
 
-@[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
-  Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
-            (fun h => h.symm ▸ Int.dvd_refl _)
-
-protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩
-
-protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm ..⟩
-
-@[simp] protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
-  constructor <;> exact fun ⟨k, e⟩ =>
-    ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
-
-protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
-  constructor <;> exact fun ⟨k, e⟩ =>
-    ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
-
-@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
-  refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
-  rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
-  cases hk <;> subst b
-  · apply Int.dvd_mul_right
-  · rw [← Int.mul_neg]; apply Int.dvd_mul_right
-
-theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
-  rw [← natAbs_dvd_natAbs, natAbs_ofNat]
-
 protected theorem dvd_add : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b + c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d + e, by rw [Int.mul_add]⟩
 
@@ -129,14 +84,6 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
 
 /-! ### *div zero  -/
 
-@[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
-  | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => show -ofNat _ = _ by simp
-
-@[simp] protected theorem ediv_zero : ∀ a : Int, a / 0 = 0
-  | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => rfl
-
 @[simp] protected theorem zero_tdiv : ∀ b : Int, tdiv 0 b = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
@@ -171,12 +118,6 @@ theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv
 
 /-! ### mod zero -/
 
-@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
-
-@[simp] theorem emod_zero : ∀ a : Int, a % 0 = a
-  | ofNat _ => congrArg ofNat <| Nat.mod_zero _
-  | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
-
 @[simp] theorem zero_tmod (b : Int) : tmod 0 b = 0 := by cases b <;> simp [tmod]
 
 @[simp] theorem tmod_zero : ∀ a : Int, tmod a 0 = a
@@ -190,39 +131,11 @@ theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv
   | succ _ => congrArg ofNat <| Nat.mod_zero _
   | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
 
-/-! ### ofNat mod -/
-
-@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
-
-
 /-! ### mod definitions -/
 
-theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
-  | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
-  | ofNat m, -[n+1] => by
-    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
-    rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
-  | -[_+1], 0 => by rw [emod_zero]; rfl
-  | -[m+1], succ n => aux m n.succ
-  | -[m+1], -[n+1] => aux m n.succ
-where
-  aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by
-    rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
-      ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
-    exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
-
-theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
-  rw [Int.mul_comm]; exact emod_add_ediv ..
-
-theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
-  rw [Int.add_comm]; exact emod_add_ediv ..
-
 theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
   rw [Int.mul_comm]; exact ediv_add_emod ..
 
-theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
-  rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
-
 theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
   | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
   | ofNat m, -[n+1] => by
@@ -288,17 +201,10 @@ theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod
 
 /-! ### `/` ediv -/
 
-@[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
-  | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
-  | ofNat _, -[_+1] => (Int.neg_neg _).symm
-  | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
-
 theorem ediv_neg' {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0 :=
   match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => negSucc_lt_zero _
 
-protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl
-
 theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b + 1) :=
   match b, eq_succ_of_zero_lt H with
   | _, ⟨_, rfl⟩ => rfl
@@ -326,61 +232,6 @@ theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0
 theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. ▸ Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
-theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b :=
-  suffices ∀ {{a b c : Int}}, 0 < c → (a + b * c).ediv c = a.ediv c + b from
-    match Int.lt_trichotomy c 0 with
-    | Or.inl hlt => by
-      rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]
-      exact this (Int.neg_pos_of_neg hlt)
-    | Or.inr (Or.inl HEq) => absurd HEq H
-    | Or.inr (Or.inr hgt) => this hgt
-  suffices ∀ {k n : Nat} {a : Int}, (a + n * k.succ).ediv k.succ = a.ediv k.succ + n from
-    fun a b c H => match c, eq_succ_of_zero_lt H, b with
-      | _, ⟨_, rfl⟩, ofNat _ => this
-      | _, ⟨k, rfl⟩, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
-        rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
-  fun {k n} => @fun
-  | ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
-  | -[m+1] => by
-    show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
-    by_cases h : m < n * k.succ
-    · rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
-      apply congrArg ofNat
-      rw [Nat.mul_comm, Nat.mul_sub_div]; rwa [Nat.mul_comm]
-    · have h := Nat.not_lt.1 h
-      have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
-        rw [negSucc_eq, Int.ofNat_sub h]
-        simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]
-      show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
-      rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
-      apply congrArg negSucc
-      rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
-
-theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
-  if h : c = 0 then by simp [h] else by
-    let ⟨k, hk⟩ := H
-    rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
-      ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
-
-theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
-  rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]
-
-@[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
-  have := Int.add_mul_ediv_right 0 a H
-  rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this
-
-@[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
-  Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
-
-
-theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0 := by
-  rw [Int.div_def]
-  match b, h with
-  | Int.ofNat (b+1), _ =>
-    rcases a with ⟨a⟩ <;> simp [Int.ediv]
-    norm_cast
-    simp
-
 theorem ediv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a / b = 0 :=
   match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@@ -442,35 +293,6 @@ theorem emod_negSucc (m : Nat) (n : Int) :
 
 theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
 
-theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
-  | ofNat _, _, _ => ofNat_zero_le _
-  | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
-
-theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
-  match a, b, eq_succ_of_zero_lt H with
-  | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
-  | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
-
-theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
-  calc k * (x / k)
-    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
-    _ = x                   := ediv_add_emod _ _
-
-theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
-  calc x
-    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
-    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
-
-@[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
-  if cz : c = 0 then by
-    rw [cz, Int.mul_zero, Int.add_zero]
-  else by
-    rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
-      Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]
-
-@[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
-  rw [Int.mul_comm, Int.add_mul_emod_self]
-
 @[simp] theorem add_neg_mul_emod_self {a b c : Int} : (a + -(b * c)) % c = a % c := by
   rw [Int.neg_mul_eq_neg_mul, add_mul_emod_self]
 
@@ -489,53 +311,9 @@ theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by
 @[simp] theorem emod_neg (a b : Int) : a % -b = a % b := by
   rw [emod_def, emod_def, Int.ediv_neg, Int.neg_mul_neg]
 
-@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
-  have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
-  rwa [Int.add_right_comm, emod_add_ediv] at this
-
-@[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
-  rw [Int.add_comm, emod_add_emod, Int.add_comm]
-
-theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n := by
-  rw [add_emod_emod, emod_add_emod]
-
-theorem add_emod_eq_add_emod_right {m n k : Int} (i : Int)
-    (H : m % n = k % n) : (m + i) % n = (k + i) % n := by
-  rw [← emod_add_emod, ← emod_add_emod k, H]
-
-theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔ m % n = k % n :=
-  ⟨fun H => by
-    have := add_emod_eq_add_emod_right (-i) H
-    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
-  add_emod_eq_add_emod_right _⟩
-
-@[simp] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
-  rw [← Int.zero_add (a * b), Int.add_mul_emod_self, Int.zero_emod]
-
-@[simp] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
-  rw [Int.mul_comm, mul_emod_left]
-
-theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
-  conv => lhs; rw [
-    ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
-    Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
-    ← Int.mul_assoc, add_mul_emod_self]
-
-@[simp] theorem emod_self {a : Int} : a % a = 0 := by
-  have := mul_emod_left 1 a; rwa [Int.one_mul] at this
-
 @[simp] theorem neg_emod_self (a : Int) : -a % a = 0 := by
   rw [neg_emod, Int.sub_self, zero_emod]
 
-@[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
-    (h : m ∣ k) : (n % k) % m = n % m := by
-  conv => rhs; rw [← emod_add_ediv n k]
-  match k, h with
-  | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
-
-@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
-  conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
-
 @[simp] theorem emod_sub_emod (m n k : Int) : (m % n - k) % n = (m - k) % n :=
   Int.emod_add_emod m n (-k)
 
@@ -543,10 +321,6 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   apply (emod_add_cancel_right (n % k)).mp
   rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel]
 
-theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
-  apply (emod_add_cancel_right b).mp
-  rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]
-
 theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
   have b0 := Int.le_trans H1 (Int.le_of_lt H2)
   match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
@@ -555,14 +329,25 @@ theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
 @[simp] theorem emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x :=
   emod_eq_of_lt h (Int.lt_succ x)
 
+theorem negSucc_emod_ofNat_succ_eq_zero_iff {a b : Nat} :
+    -[a+1] % (b + 1 : Int) = 0 ↔ (a + 1) % (b + 1) = 0 := by
+  rw [← natCast_one, ← natCast_add]
+  change Int.emod _ _ = 0 ↔ _
+  rw [emod, natAbs_ofNat]
+  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
+  rw [eq_comm]
+  apply Nat.succ_mod_succ_eq_zero_iff.symm
+
+theorem negSucc_emod_negSucc_eq_zero_iff {a b : Nat} :
+    -[a+1] % -[b+1] = 0 ↔ (a + 1) % (b + 1) = 0 := by
+  change Int.emod _ _ = 0 ↔ _
+  rw [emod, natAbs_negSucc]
+  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
+  rw [eq_comm]
+  apply Nat.succ_mod_succ_eq_zero_iff.symm
+
 /-! ### properties of `/` and `%` -/
 
-theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
-  have := emod_add_ediv a b; rwa [H, Int.zero_add] at this
-
-theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
-  rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]
-
 theorem emod_two_eq (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by
   have h₁ : 0 ≤ x % 2 := Int.emod_nonneg x (by decide)
   have h₂ : x % 2 < 2 := Int.emod_lt_of_pos x (by decide)
@@ -616,19 +401,10 @@ theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a := by
   have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)
   rwa [natAbs_of_nonneg Ha] at this
 
-theorem dvd_of_emod_eq_zero {a b : Int} (H : b % a = 0) : a ∣ b :=
-  ⟨b / a, (mul_ediv_cancel_of_emod_eq_zero H).symm⟩
-
 theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ x % m - x := by
   apply dvd_of_emod_eq_zero
   simp [sub_emod]
 
-theorem emod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → b % a = 0
-  | _, _, ⟨_, rfl⟩ => mul_emod_right ..
-
-theorem dvd_iff_emod_eq_zero {a b : Int} : a ∣ b ↔ b % a = 0 :=
-  ⟨emod_eq_zero_of_dvd, dvd_of_emod_eq_zero⟩
-
 @[simp] theorem neg_mul_emod_left (a b : Int) : -(a * b) % b = 0 := by
   rw [← dvd_iff_emod_eq_zero, Int.dvd_neg]
   exact Int.dvd_mul_left a b
@@ -646,32 +422,12 @@ theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a :
   · simp_all
   · exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
 
-protected theorem mul_ediv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b) / c = a * (b / c)
-  | _, c, ⟨d, rfl⟩ =>
-    if cz : c = 0 then by simp [cz, Int.mul_zero] else by
-      rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]
-
-protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
-    (h : c ∣ a) : (a * b) / c = a / c * b := by
-  rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]
-
-theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
-  | _, b, ⟨c, rfl⟩ => by
-    by_cases bz : b = 0
-    · simp [bz]
-    · rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
-
 @[simp] theorem neg_mul_ediv_cancel (a b : Int) (h : b ≠ 0) : -(a * b) / b = -a := by
   rw [neg_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ h]
 
 @[simp] theorem neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b := by
   rw [neg_ediv_of_dvd (Int.dvd_mul_right a b), mul_ediv_cancel_left _ h]
 
-theorem sub_ediv_of_dvd (a : Int) {b c : Int}
-    (hcb : c ∣ b) : (a - b) / c = a / c - b / c := by
-  rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
-  congr; exact Int.neg_ediv_of_dvd hcb
-
 @[simp] theorem ediv_one : ∀ a : Int, a / 1 = a
   | (_:Nat) => congrArg Nat.cast (Nat.div_one _)
   | -[_+1]  => congrArg negSucc (Nat.div_one _)
@@ -705,12 +461,6 @@ theorem dvd_sub_of_emod_eq {a b c : Int} (h : a % b = c) : b ∣ a - c := by
   rw [Int.emod_emod, ← emod_sub_cancel_right c, Int.sub_self, zero_emod] at hx
   exact dvd_of_emod_eq_zero hx
 
-protected theorem ediv_mul_cancel {a b : Int} (H : b ∣ a) : a / b * b = a :=
-  ediv_mul_cancel_of_emod_eq_zero (emod_eq_zero_of_dvd H)
-
-protected theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b := by
-  rw [Int.mul_comm, Int.ediv_mul_cancel H]
-
 protected theorem eq_mul_of_ediv_eq_right {a b c : Int}
     (H1 : b ∣ a) (H2 : a / b = c) : a = b * c := by rw [← H2, Int.mul_ediv_cancel' H1]
 
@@ -1092,21 +842,10 @@ theorem fdiv_eq_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b = a / b
 
 /-! ### bmod -/
 
-@[simp] theorem bmod_emod : bmod x m % m = x % m := by
-  dsimp [bmod]
-  split <;> simp [Int.sub_emod]
-
 @[simp]
 theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n := by
   simp [bmod, Int.emod_emod]
 
-theorem bmod_def (x : Int) (m : Nat) : bmod x m =
-  if (x % m) < (m + 1) / 2 then
-    x % m
-  else
-    (x % m) - m :=
-  rfl
-
 theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
   unfold bdiv bmod
   split

src/Init/Data/Int/Gcd.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Int.Basic
 import Init.Data.Nat.Gcd
 import Init.Data.Nat.Lcm
-import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivMod.Lemmas
 
 /-!
 Definition and lemmas for gcd and lcm over Int

src/Init/Data/Int/Lemmas.lean

@@ -129,7 +129,16 @@ theorem subNatNat_of_le {m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n) :
 theorem subNatNat_of_lt {m n : Nat} (h : m < n) : subNatNat m n = -[pred (n - m) +1] :=
   subNatNat_of_sub_eq_succ <| (Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)).symm
 
-
+@[simp] theorem subNat_eq_zero_iff {a b : Nat} : subNatNat a b = 0 ↔ a = b := by
+  cases Nat.lt_or_ge a b with
+  | inl h =>
+    rw [subNatNat_of_lt h]
+    simpa using ne_of_lt h
+  | inr h =>
+    rw [subNatNat_of_le h]
+    norm_cast
+    rw [Nat.sub_eq_iff_eq_add' h]
+    simp
 
 /- # Additive group properties -/
 

src/Init/Data/Int/LemmasAux.lean

@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 prelude
 import Init.Data.Int.Order
+import Init.Data.Int.DivMod.Lemmas
 import Init.Omega
 
 

src/Init/Data/Int/Linear.lean

@@ -8,7 +8,7 @@ import Init.ByCases
 import Init.Data.Prod
 import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
-import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.Gcd
 import Init.Data.RArray
 import Init.Data.AC

src/Init/Data/Nat/Lemmas.lean

@@ -1016,6 +1016,39 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   · exact (m % 0).div_zero
   · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
 
+theorem mod_eq_iff {a b c : Nat} :
+    a % b = c ↔ (b = 0 ∧ a = c) ∨ (c < b ∧ Exists fun k => a = b * k + c) :=
+  ⟨fun h =>
+    if w : b = 0 then
+      .inl ⟨w, by simpa [w] using h⟩
+    else
+      .inr ⟨by subst h; exact Nat.mod_lt a (zero_lt_of_ne_zero w),
+        a / b, by subst h; exact (div_add_mod a b).symm⟩,
+   by
+     rintro (⟨rfl, rfl⟩ | ⟨w, h, rfl⟩)
+     · simp_all
+     · rw [mul_add_mod, mod_eq_of_lt w]⟩
+
+theorem succ_mod_succ_eq_zero_iff {a b : Nat} :
+    (a + 1) % (b + 1) = 0 ↔ a % (b + 1) = b := by
+  symm
+  rw [mod_eq_iff, mod_eq_iff]
+  simp only [add_one_ne_zero, false_and, Nat.lt_add_one, true_and, false_or, and_self, zero_lt_succ,
+    Nat.add_zero]
+  constructor
+  · rintro ⟨k, rfl⟩
+    refine ⟨k + 1, ?_⟩
+    simp [Nat.add_mul, Nat.mul_add, Nat.add_assoc]
+  · rintro ⟨k, h⟩
+    cases k with
+    | zero => simp at h
+    | succ k =>
+      refine ⟨k, ?_⟩
+      simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc,
+        Nat.add_right_cancel_iff] at h
+      subst h
+      simp [Nat.add_mul]
+
 /-! ### Decidability of predicates -/
 
 instance decidableBallLT :

src/Init/Omega/Int.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 prelude
-import Init.Data.Int.DivMod
+import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.Order
 
 /-!

src/Init/Omega/IntList.lean

@@ -5,7 +5,7 @@ Authors: Kim Morrison
 -/
 prelude
 import Init.Data.List.Zip
-import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Nat.Gcd
 
 namespace Lean.Omega

src/Std/Internal/Rat.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.NotationExtra
 import Init.Data.ToString.Macro
-import Init.Data.Int.DivMod
+import Init.Data.Int.DivMod.Basic
 import Init.Data.Nat.Gcd
 namespace Std
 namespace Internal

src/Std/Time/Internal/Bounded.lean

@@ -5,6 +5,7 @@ Authors: Sofia Rodrigues
 -/
 prelude
 import Init.Omega
+import Init.Data.Int.DivMod.Lemmas
 
 namespace Std
 namespace Time