diff --git a/src/Init/Data/Int/DivMod.lean b/src/Init/Data/Int/DivMod.lean
index 2ca0ceffd5a2..c6a7b21ca734 100644
--- a/src/Init/Data/Int/DivMod.lean
+++ b/src/Init/Data/Int/DivMod.lean
@@ -4,338 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 prelude
-<<<<<<< HEAD
 import Init.Data.Int.DivMod.Basic
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.DivMod.Lemmas
-=======
-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
->>>>>>> origin/master
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 8bbfa9f1038d..c85b30c9634f 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -374,7 +374,6 @@ theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
 -- @[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
 --   Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
 
-<<<<<<< HEAD:src/Init/Data/Int/DivMod/Lemmas.lean
 -- 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
@@ -382,16 +381,6 @@ theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
 --     rcases a with ⟨a⟩ <;> simp [Int.ediv]
 --     norm_cast
 --     simp
-=======
-
-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
->>>>>>> origin/master:src/Init/Data/Int/DivModLemmas.lean
 
 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