fixes to tests

src/Init/Data/Int.lean

@@ -5,3 +5,9 @@ Authors: Leonardo de Moura
 -/
 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.Order

src/Init/Data/Int/Basic.lean

@@ -53,8 +53,29 @@ instance instOfNat : OfNat Int n where
   ofNat := Int.ofNat n
 
 namespace Int
+
+/--
+`-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
+`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
+-/
+scoped notation "-[" n "+1]" => negSucc n
+
 instance : Inhabited Int := ⟨ofNat 0⟩
 
+@[simp] theorem default_eq_zero : default = (0 : Int) := rfl
+
+protected theorem zero_ne_one : (0 : Int) ≠ 1 := nofun
+
+/-! ## Coercions -/
+
+@[simp] theorem ofNat_eq_coe : Int.ofNat n = Nat.cast n := rfl
+
+@[simp] theorem ofNat_zero : ((0 : Nat) : Int) = 0 := rfl
+
+@[simp] theorem ofNat_one  : ((1 : Nat) : Int) = 1 := rfl
+
+theorem ofNat_two : ((2 : Nat) : Int) = 2 := rfl
+
 /-- Negation of a natural number. -/
 def negOfNat : Nat → Int
   | 0      => 0
@@ -100,10 +121,10 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_int_add"]
 protected def add (m n : @& Int) : Int :=
   match m, n with
-  | ofNat m,   ofNat n   => ofNat (m + n)
-  | ofNat m,   negSucc n => subNatNat m (succ n)
-  | negSucc m, ofNat n   => subNatNat n (succ m)
-  | negSucc m, negSucc n => negSucc (succ (m + n))
+  | ofNat m, ofNat n => ofNat (m + n)
+  | ofNat m, -[n +1] => subNatNat m (succ n)
+  | -[m +1], ofNat n => subNatNat n (succ m)
+  | -[m +1], -[n +1] => negSucc (succ (m + n))
 
 instance : Add Int where
   add := Int.add
@@ -121,10 +142,10 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_int_mul"]
 protected def mul (m n : @& Int) : Int :=
   match m, n with
-  | ofNat m,   ofNat n   => ofNat (m * n)
-  | ofNat m,   negSucc n => negOfNat (m * succ n)
-  | negSucc m, ofNat n   => negOfNat (succ m * n)
-  | negSucc m, negSucc n => ofNat (succ m * succ n)
+  | ofNat m, ofNat n => ofNat (m * n)
+  | ofNat m, -[n +1] => negOfNat (m * succ n)
+  | -[m +1], ofNat n => negOfNat (succ m * n)
+  | -[m +1], -[n +1] => ofNat (succ m * succ n)
 
 instance : Mul Int where
   mul := Int.mul
@@ -139,8 +160,7 @@ instance : Mul Int where
 
   Implemented by efficient native code. -/
 @[extern "lean_int_sub"]
-protected def sub (m n : @& Int) : Int :=
-  m + (- n)
+protected def sub (m n : @& Int) : Int := m + (- n)
 
 instance : Sub Int where
   sub := Int.sub
@@ -178,11 +198,11 @@ protected def decEq (a b : @& Int) : Decidable (a = b) :=
   | ofNat a, ofNat b => match decEq a b with
     | isTrue h  => isTrue  <| h ▸ rfl
     | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
-  | negSucc a, negSucc b => match decEq a b with
+  | ofNat _, -[_ +1] => isFalse <| fun h => Int.noConfusion h
+  | -[_ +1], ofNat _ => isFalse <| fun h => Int.noConfusion h
+  | -[a +1], -[b +1] => match decEq a b with
     | isTrue h  => isTrue  <| h ▸ rfl
     | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
-  | ofNat _, negSucc _ => isFalse <| fun h => Int.noConfusion h
-  | negSucc _, ofNat _ => isFalse <| fun h => Int.noConfusion h
 
 instance : DecidableEq Int := Int.decEq
 
@@ -199,8 +219,8 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_int_dec_nonneg"]
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
-  | ofNat m   => isTrue <| NonNeg.mk m
-  | negSucc _ => isFalse <| fun h => nomatch h
+  | ofNat m => isTrue <| NonNeg.mk m
+  | -[_ +1] => isFalse <| fun h => nomatch h
 
 /-- Decides whether `a ≤ b`.
 
@@ -241,85 +261,21 @@ set_option bootstrap.genMatcherCode false in
 @[extern "lean_nat_abs"]
 def natAbs (m : @& Int) : Nat :=
   match m with
-  | ofNat m   => m
-  | negSucc m => m.succ
+  | ofNat m => m
+  | -[m +1] => m.succ
 
-/-- Integer division. This function 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.
+/-! ## sign -/
 
-  The relation between integer division and modulo is found in [the
-  `Int.mod_add_div` theorem in std][theo mod_add_div] which states
-  that `a % b + b * (a / b) = a`, unconditionally.
+/--
+Returns the "sign" of the integer as another integer: `1` for positive numbers,
+`-1` for negative numbers, and `0` for `0`.
+-/
+def sign : Int → Int
+  | Int.ofNat (succ _) => 1
+  | Int.ofNat 0 => 0
+  | -[_+1]      => -1
 
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
-
-  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) -- -1
-  #eval (-12 : Int) / (-7 : Int) -- 1
-  ```
-
-  Implemented by efficient native code. -/
-@[extern "lean_int_div"]
-def div : (@& Int) → (@& Int) → Int
-  | ofNat m,   ofNat n   => ofNat (m / n)
-  | ofNat m,   negSucc n => -ofNat (m / succ n)
-  | negSucc m, ofNat n   => -ofNat (succ m / n)
-  | negSucc m, negSucc n => ofNat (succ m / succ n)
-
-instance : Div Int where
-  div := Int.div
-
-/-- Integer modulo. This function uses the
-  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
-  to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
-  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
-  particular, `a % 0 = a`.
-
-  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
-  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
-
-  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_mod"]
-def mod : (@& Int) → (@& Int) → Int
-  | ofNat m,   ofNat n   => ofNat (m % n)
-  | ofNat m,   negSucc n => ofNat (m % succ n)
-  | negSucc m, ofNat n   => -ofNat (succ m % n)
-  | negSucc m, negSucc n => -ofNat (succ m % succ n)
-
-instance : Mod Int where
-  mod := Int.mod
+/-! ## Conversion -/
 
 /-- Turns an integer into a natural number, negative numbers become
   `0`.
@@ -334,6 +290,25 @@ def toNat : Int → Nat
   | ofNat n   => n
   | negSucc _ => 0
 
+/--
+* If `n : Nat`, then `int.toNat' n = some n`
+* If `n : Int` is negative, then `int.toNat' n = none`.
+-/
+def toNat' : Int → Option Nat
+  | (n : Nat) => some n
+  | -[_+1] => none
+
+/-! ## divisibility -/
+
+/--
+Divisibility of integers. `a ∣ b` (typed as `\|`) says that
+there is some `c` such that `b = a * c`.
+-/
+instance : Dvd Int where
+  dvd a b := Exists (fun c => b = a * c)
+
+/-! ## Powers -/
+
 /-- Power of an integer to some natural number.
 
   ```

src/Init/Data/Int/Bitwise.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Basic
+import Init.Data.Nat.Bitwise
+
+namespace Int
+
+/-! ## bit operations -/
+
+/--
+Bitwise not
+
+Interprets the integer as an infinite sequence of bits in two's complement
+and complements each bit.
+```
+~~~(0:Int) = -1
+~~~(1:Int) = -2
+~~~(-1:Int) = 0
+```
+-/
+protected def not : Int -> Int
+  | Int.ofNat n => Int.negSucc n
+  | Int.negSucc n => Int.ofNat n
+
+instance : Complement Int := ⟨.not⟩
+
+/--
+Bitwise shift right.
+
+Conceptually, this treats the integer as an infinite sequence of bits in two's
+complement and shifts the value to the right.
+
+```lean
+( 0b0111:Int) >>> 1 =  0b0011
+( 0b1000:Int) >>> 1 =  0b0100
+(-0b1000:Int) >>> 1 = -0b0100
+(-0b0111:Int) >>> 1 = -0b0100
+```
+-/
+protected def shiftRight : Int → Nat → Int
+  | Int.ofNat n, s => Int.ofNat (n >>> s)
+  | Int.negSucc n, s => Int.negSucc (n >>> s)
+
+instance : HShiftRight Int Nat Int := ⟨.shiftRight⟩
+
+end Int

src/Init/Data/Int/DivMod.lean

@@ -0,0 +1,159 @@
+/-
+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`.
+-/
+
+/-! ### T-rounding division -/
+
+/--
+`div` 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.mod_add_div` which states that
+  `a % b + b * (a / b) = a`, unconditionally.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo
+  mod_add_div]:
+  https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  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) -- -1
+  #eval (-12 : Int) / (-7 : Int) -- 1
+  ```
+
+  Implemented by efficient native code.
+-/
+@[extern "lean_int_div"]
+def div : (@& 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.div`, meaning that `a % b + b * (a / b) = a`
+  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
+  particular, `a % 0 = a`.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  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_mod"]
+def mod : (@& 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)
+
+/-! ### 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`.
+-/
+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`.
+-/
+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)
+
+/-! ### 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`.
+-/
+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`.
+-/
+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
+
+end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -0,0 +1,347 @@
+/-
+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
+import Init.Data.Int.Order
+import Init.Data.Nat.Dvd
+import Init.RCases
+import Init.TacticsExtra
+
+/-!
+# Lemmas about integer division needed to bootstrap `omega`.
+-/
+
+
+open Nat (succ)
+
+namespace Int
+
+/-! ### `/`  -/
+
+@[simp] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+
+@[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 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 m, -[n+1] => (Int.neg_neg _).symm
+  | ofNat m, succ n | -[m+1], 0 | -[m+1], succ n | -[m+1], -[n+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 m => 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)
+    if h : m < n * k.succ then
+      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]
+    else
+      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]
+    exact decide_eq_decide.mp rfl
+
+/-! ### mod -/
+
+theorem mod_def' (m n : Int) : m % n = emod m n := rfl
+
+theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
+
+theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
+
+@[simp] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+
+@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := by simp [mod_def', emod]
+
+@[simp] theorem emod_zero : ∀ a : Int, a % 0 = a
+  | ofNat _ => congrArg ofNat <| Nat.mod_zero _
+  | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
+
+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 ediv_add_emod (a b : Int) : b * (a / b) + a % b = a :=
+  (Int.add_comm ..).trans (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]
+
+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) _
+
+theorem emod_add_ediv' (m k : Int) : m % k + m / k * k = m := by
+  rw [Int.mul_comm]; apply emod_add_ediv
+
+@[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_emod_self {a b : Int} : (a + b) % b = a % b := by
+  have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
+
+@[simp] theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a := by
+  rw [Int.add_comm, Int.add_emod_self]
+
+theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by
+  rw [← add_emod_self_left]; rfl
+
+@[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]
+
+@[local 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]
+
+/-! ### dvd -/
+
+protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
+
+protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
+
+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⟩ => ⟨d * e, by rw [Int.mul_assoc]⟩
+
+@[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
+  ⟨fun ⟨k, e⟩ => by rw [e, Int.zero_mul], fun h => h.symm ▸ Int.dvd_refl _⟩
+
+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]⟩
+
+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 ..⟩
+
+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]⟩
+
+protected theorem dvd_sub : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b - c
+  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Int.mul_sub]⟩
+
+
+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] 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]
+
+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⟩
+
+theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
+  rw [dvd_iff_emod_eq_zero] at h
+  if w : a = 0 then simp_all
+  else exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
+
+instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
+  decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
+
+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 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 if bz : b = 0 then simp [bz] else
+    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
+
+/-!
+# `bmod` ("balanced" mod)
+
+We use balanced mod in the omega algorithm,
+to make ±1 coefficients appear in equations without them.
+-/
+
+/--
+Balanced mod, taking values in the range [- m/2, (m - 1)/2].
+-/
+def bmod (x : Int) (m : Nat) : Int :=
+  let r := x % m
+  if r < (m + 1) / 2 then
+    r
+  else
+    r - m
+
+@[simp] theorem bmod_emod : bmod x m % m = x % m := by
+  dsimp [bmod]
+  split <;> simp [Int.sub_emod]

src/Init/Data/Int/Gcd.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Basic
+import Init.Data.Nat.Gcd
+
+namespace Int
+
+/-! ## gcd -/
+
+/-- Computes the greatest common divisor of two integers, as a `Nat`. -/
+def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs
+
+end Int

src/Init/Data/Int/Lemmas.lean

@@ -0,0 +1,500 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Basic
+import Init.Conv
+import Init.PropLemmas
+
+namespace Int
+
+open Nat
+
+/-! ## Definitions of basic functions -/
+
+theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = ↑(m - n) := by
+  rw [subNatNat, h, ofNat_eq_coe]
+
+theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1] := by
+  rw [subNatNat, h]
+
+@[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl
+
+theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
+theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
+theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
+
+@[local simp] theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
+@[local simp] theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
+@[local simp] theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
+
+theorem negSucc_coe (n : Nat) : -[n+1] = -↑(n + 1) := rfl
+
+theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
+
+/-! ## These are only for internal use -/
+
+@[simp] theorem add_def {a b : Int} : Int.add a b = a + b := rfl
+
+@[local simp] theorem ofNat_add_ofNat (m n : Nat) : (↑m + ↑n : Int) = ↑(m + n) := rfl
+@[local simp] theorem ofNat_add_negSucc (m n : Nat) : ↑m + -[n+1] = subNatNat m (succ n) := rfl
+@[local simp] theorem negSucc_add_ofNat (m n : Nat) : -[m+1] + ↑n = subNatNat n (succ m) := rfl
+@[local simp] theorem negSucc_add_negSucc (m n : Nat) : -[m+1] + -[n+1] = -[succ (m + n) +1] := rfl
+
+@[simp] theorem mul_def {a b : Int} : Int.mul a b = a * b := rfl
+
+@[local simp] theorem ofNat_mul_ofNat (m n : Nat) : (↑m * ↑n : Int) = ↑(m * n) := rfl
+@[local simp] theorem ofNat_mul_negSucc' (m n : Nat) : ↑m * -[n+1] = negOfNat (m * succ n) := rfl
+@[local simp] theorem negSucc_mul_ofNat' (m n : Nat) : -[m+1] * ↑n = negOfNat (succ m * n) := rfl
+@[local simp] theorem negSucc_mul_negSucc' (m n : Nat) :
+    -[m+1] * -[n+1] = ofNat (succ m * succ n) := rfl
+
+/- ## some basic functions and properties -/
+
+theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
+
+theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj
+
+theorem ofNat_ne_zero : ((n : Nat) : Int) ≠ 0 ↔ n ≠ 0 := not_congr ofNat_eq_zero
+
+theorem negSucc_inj : negSucc m = negSucc n ↔ m = n := ⟨negSucc.inj, fun H => by simp [H]⟩
+
+theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
+
+@[simp] theorem negSucc_ne_zero (n : Nat) : -[n+1] ≠ 0 := nofun
+
+@[simp] theorem zero_ne_negSucc (n : Nat) : 0 ≠ -[n+1] := nofun
+
+@[simp] theorem Nat.cast_ofNat_Int :
+  (Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n := rfl
+
+/- ## neg -/
+
+@[simp] protected theorem neg_neg : ∀ a : Int, -(-a) = a
+  | 0      => rfl
+  | succ _ => rfl
+  | -[_+1] => rfl
+
+protected theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
+  ⟨fun h => by rw [← Int.neg_neg a, ← Int.neg_neg b, h], congrArg _⟩
+
+@[simp] protected theorem neg_eq_zero : -a = 0 ↔ a = 0 := Int.neg_inj (b := 0)
+
+protected theorem neg_ne_zero : -a ≠ 0 ↔ a ≠ 0 := not_congr Int.neg_eq_zero
+
+protected theorem sub_eq_add_neg {a b : Int} : a - b = a + -b := rfl
+
+theorem add_neg_one (i : Int) : i + -1 = i - 1 := rfl
+
+/- ## basic properties of subNatNat -/
+
+-- @[elabAsElim] -- TODO(Mario): unexpected eliminator resulting type
+theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
+    (hp : ∀ i n, motive (n + i) n i)
+    (hn : ∀ i m, motive m (m + i + 1) -[i+1]) :
+    motive m n (subNatNat m n) := by
+  unfold subNatNat
+  match h : n - m with
+  | 0 =>
+    have ⟨k, h⟩ := Nat.le.dest (Nat.le_of_sub_eq_zero h)
+    rw [h.symm, Nat.add_sub_cancel_left]; apply hp
+  | succ k =>
+    rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h
+    rw [h, Nat.add_comm]; apply hn
+
+theorem subNatNat_add_left : subNatNat (m + n) m = n := by
+  unfold subNatNat
+  rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]
+
+theorem subNatNat_add_right : subNatNat m (m + n + 1) = negSucc n := by
+  simp [subNatNat, Nat.add_assoc, Nat.add_sub_cancel_left]
+
+theorem subNatNat_add_add (m n k : Nat) : subNatNat (m + k) (n + k) = subNatNat m n := by
+  apply subNatNat_elim m n (fun m n i => subNatNat (m + k) (n + k) = i)
+  focus
+    intro i j
+    rw [Nat.add_assoc, Nat.add_comm i k, ← Nat.add_assoc]
+    exact subNatNat_add_left
+  focus
+    intro i j
+    rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]
+    exact subNatNat_add_right
+
+theorem subNatNat_of_le {m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n) :=
+  subNatNat_of_sub_eq_zero (Nat.sub_eq_zero_of_le h)
+
+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
+
+/- # Additive group properties -/
+
+/- addition -/
+
+protected theorem add_comm : ∀ a b : Int, a + b = b + a
+  | ofNat n, ofNat m => by simp [Nat.add_comm]
+  | ofNat _, -[_+1]  => rfl
+  | -[_+1],  ofNat _ => rfl
+  | -[_+1],  -[_+1]  => by simp [Nat.add_comm]
+
+@[simp] protected theorem add_zero : ∀ a : Int, a + 0 = a
+  | ofNat _ => rfl
+  | -[_+1]  => rfl
+
+@[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. ▸ a.add_zero
+
+theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
+  show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]
+
+theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat m (k + n) := by
+  rwa [← subNatNat_add_add _ _ n, Nat.sub_add_cancel]
+
+theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
+  cases n.lt_or_ge k with
+  | inl h' =>
+    simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
+    conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
+    apply subNatNat_add_add
+  | inr h' => simp [subNatNat_of_le h',
+      subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']
+
+theorem subNatNat_add_negSucc (m n k : Nat) :
+    subNatNat m n + -[k+1] = subNatNat m (n + succ k) := by
+  have h := Nat.lt_or_ge m n
+  cases h with
+  | inr h' =>
+    rw [subNatNat_of_le h']
+    simp
+    rw [subNatNat_sub h', Nat.add_comm]
+  | inl h' =>
+    have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
+    have h₃ : m ≤ n + k := le_of_succ_le_succ h₂
+    rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
+    simp [Nat.add_comm]
+    rw [← add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃,
+      Nat.pred_succ]
+    rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
+
+protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
+  | (m:Nat), (n:Nat), c => aux1 ..
+  | Nat.cast m, b, Nat.cast k => by
+    rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]
+  | a, (n:Nat), (k:Nat) => by
+    rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]
+  | -[m+1], -[n+1], (k:Nat) => aux2 ..
+  | -[m+1], (n:Nat), -[k+1] => by
+    rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]
+  | (m:Nat), -[n+1], -[k+1] => by
+    rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
+  | -[m+1], -[n+1], -[k+1] => by
+    simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
+where
+  aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
+    | (k:Nat) => by simp [Nat.add_assoc]
+    | -[k+1]  => by simp [subNatNat_add]
+  aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
+    simp [add_succ]
+    rw [Int.add_comm, subNatNat_add_negSucc]
+    simp [add_succ, succ_add, Nat.add_comm]
+
+protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
+  rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
+
+protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by
+  rw [Int.add_assoc, Int.add_comm b, ← Int.add_assoc]
+
+/- ## negation -/
+
+theorem subNatNat_self : ∀ n, subNatNat n n = 0
+  | 0      => rfl
+  | succ m => by rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]
+
+attribute [local simp] subNatNat_self
+
+@[local simp] protected theorem add_left_neg : ∀ a : Int, -a + a = 0
+  | 0      => rfl
+  | succ m => by simp
+  | -[m+1] => by simp
+
+@[local simp] protected theorem add_right_neg (a : Int) : a + -a = 0 := by
+  rw [Int.add_comm, Int.add_left_neg]
+
+@[simp] protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
+  rw [← Int.add_zero (-a), ← h, ← Int.add_assoc, Int.add_left_neg, Int.zero_add]
+
+protected theorem eq_neg_of_eq_neg {a b : Int} (h : a = -b) : b = -a := by
+  rw [h, Int.neg_neg]
+
+protected theorem eq_neg_comm {a b : Int} : a = -b ↔ b = -a :=
+  ⟨Int.eq_neg_of_eq_neg, Int.eq_neg_of_eq_neg⟩
+
+protected theorem neg_eq_comm {a b : Int} : -a = b ↔ -b = a := by
+  rw [eq_comm, Int.eq_neg_comm, eq_comm]
+
+protected theorem neg_add_cancel_left (a b : Int) : -a + (a + b) = b := by
+  rw [← Int.add_assoc, Int.add_left_neg, Int.zero_add]
+
+protected theorem add_neg_cancel_left (a b : Int) : a + (-a + b) = b := by
+  rw [← Int.add_assoc, Int.add_right_neg, Int.zero_add]
+
+protected theorem add_neg_cancel_right (a b : Int) : a + b + -b = a := by
+  rw [Int.add_assoc, Int.add_right_neg, Int.add_zero]
+
+protected theorem neg_add_cancel_right (a b : Int) : a + -b + b = a := by
+  rw [Int.add_assoc, Int.add_left_neg, Int.add_zero]
+
+protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := by
+  have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
+  simp [← Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁; exact h₁
+
+@[local simp] protected theorem neg_add {a b : Int} : -(a + b) = -a + -b := by
+  apply Int.add_left_cancel (a := a + b)
+  rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
+    Int.add_right_neg, Int.add_zero, Int.add_right_neg]
+
+/- ## subtraction -/
+
+@[simp] theorem negSucc_sub_one (n : Nat) : -[n+1] - 1 = -[n + 1 +1] := rfl
+
+@[simp] protected theorem sub_self (a : Int) : a - a = 0 := by
+  rw [Int.sub_eq_add_neg, Int.add_right_neg]
+
+@[simp] protected theorem sub_zero (a : Int) : a - 0 = a := by simp [Int.sub_eq_add_neg]
+
+@[simp] protected theorem zero_sub (a : Int) : 0 - a = -a := by simp [Int.sub_eq_add_neg]
+
+protected theorem sub_eq_zero_of_eq {a b : Int} (h : a = b) : a - b = 0 := by
+  rw [h, Int.sub_self]
+
+protected theorem eq_of_sub_eq_zero {a b : Int} (h : a - b = 0) : a = b := by
+  have : 0 + b = b := by rw [Int.zero_add]
+  have : a - b + b = b := by rwa [h]
+  rwa [Int.sub_eq_add_neg, Int.neg_add_cancel_right] at this
+
+protected theorem sub_eq_zero {a b : Int} : a - b = 0 ↔ a = b :=
+  ⟨Int.eq_of_sub_eq_zero, Int.sub_eq_zero_of_eq⟩
+
+protected theorem sub_sub (a b c : Int) : a - b - c = a - (b + c) := by
+  simp [Int.sub_eq_add_neg, Int.add_assoc]
+
+protected theorem neg_sub (a b : Int) : -(a - b) = b - a := by
+  simp [Int.sub_eq_add_neg, Int.add_comm]
+
+protected theorem sub_sub_self (a b : Int) : a - (a - b) = b := by
+  simp [Int.sub_eq_add_neg, ← Int.add_assoc]
+
+protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_add_neg]
+
+@[simp] protected theorem sub_add_cancel (a b : Int) : a - b + b = a :=
+  Int.neg_add_cancel_right a b
+
+@[simp] protected theorem add_sub_cancel (a b : Int) : a + b - b = a :=
+  Int.add_neg_cancel_right a b
+
+protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
+  rw [Int.sub_eq_add_neg, Int.add_assoc, ← Int.sub_eq_add_neg]
+
+theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
+  match m with
+  | 0 => rfl
+  | succ m =>
+    show ofNat (n - succ m) = subNatNat n (succ m)
+    rw [subNatNat, Nat.sub_eq_zero_of_le h]
+
+theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
+  rw [Int.sub_eq_add_neg, ← Int.neg_add]; rfl
+
+protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
+  apply subNatNat_elim m n fun m n i => i = m - n
+  · intros i n
+    rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
+      Int.add_right_neg, Int.add_zero]
+  · intros i n
+    simp only [negSucc_coe, ofNat_add, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
+    rw [← @Int.sub_eq_add_neg n, ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
+    apply Nat.le_refl
+
+theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
+  rw [← Int.subNatNat_eq_coe]
+  refine subNatNat_elim m n (fun m n i => toNat i = m - n) (fun i n => ?_) (fun i n => ?_)
+  · exact (Nat.add_sub_cancel_left ..).symm
+  · dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl
+
+/- ## Ring properties -/
+
+@[simp] theorem ofNat_mul_negSucc (m n : Nat) : (m : Int) * -[n+1] = -↑(m * succ n) := rfl
+
+@[simp] theorem negSucc_mul_ofNat (m n : Nat) : -[m+1] * n = -↑(succ m * n) := rfl
+
+@[simp] theorem negSucc_mul_negSucc (m n : Nat) : -[m+1] * -[n+1] = succ m * succ n := rfl
+
+protected theorem mul_comm (a b : Int) : a * b = b * a := by
+  cases a <;> cases b <;> simp [Nat.mul_comm]
+
+theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
+  cases n <;> rfl
+
+theorem negOfNat_mul_ofNat (m n : Nat) : negOfNat m * (n : Nat) = negOfNat (m * n) := by
+  rw [Int.mul_comm]; simp [ofNat_mul_negOfNat, Nat.mul_comm]
+
+theorem negSucc_mul_negOfNat (m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m * n) := by
+  cases n <;> rfl
+
+theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m) := by
+  rw [Int.mul_comm, negSucc_mul_negOfNat, Nat.mul_comm]
+
+attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
+  negSucc_mul_negOfNat negOfNat_mul_negSucc
+
+protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
+  cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
+
+protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
+  rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]
+
+protected theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b := by
+  rw [Int.mul_assoc, Int.mul_assoc, Int.mul_comm b]
+
+@[simp] protected theorem mul_zero (a : Int) : a * 0 = 0 := by cases a <;> rfl
+
+@[simp] protected theorem zero_mul (a : Int) : 0 * a = 0 := Int.mul_comm .. ▸ a.mul_zero
+
+theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases n <;> rfl
+
+theorem ofNat_mul_subNatNat (m n k : Nat) :
+    m * subNatNat n k = subNatNat (m * n) (m * k) := by
+  cases m with
+  | zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
+  | succ m => cases n.lt_or_ge k with
+    | inl h =>
+      have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
+      simp [subNatNat_of_lt h, subNatNat_of_lt h']
+      rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
+        ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
+    | inr h =>
+      have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
+      simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]
+
+theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n) := by
+  cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl
+
+theorem negSucc_mul_subNatNat (m n k : Nat) :
+    -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n) := by
+  cases n.lt_or_ge k with
+  | inl h =>
+    have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
+    rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
+    simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
+  | inr h => cases Nat.lt_or_ge k n with
+    | inl h' =>
+      have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
+      rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
+        Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
+    | inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]
+
+attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat
+
+protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
+  | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
+  | (m:Nat), (n:Nat), -[k+1]  => by
+    simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
+  | (m:Nat), -[n+1],  (k:Nat) => by
+    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
+  | (m:Nat), -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+  | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
+  | -[m+1],  (n:Nat), -[k+1]  => by
+    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
+  | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
+  | -[m+1],  -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+
+protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
+  simp [Int.mul_comm, Int.mul_add]
+
+protected theorem neg_mul_eq_neg_mul (a b : Int) : -(a * b) = -a * b :=
+  Int.neg_eq_of_add_eq_zero <| by rw [← Int.add_mul, Int.add_right_neg, Int.zero_mul]
+
+protected theorem neg_mul_eq_mul_neg (a b : Int) : -(a * b) = a * -b :=
+  Int.neg_eq_of_add_eq_zero <| by rw [← Int.mul_add, Int.add_right_neg, Int.mul_zero]
+
+@[local simp] protected theorem neg_mul (a b : Int) : -a * b = -(a * b) :=
+  (Int.neg_mul_eq_neg_mul a b).symm
+
+@[local simp] protected theorem mul_neg (a b : Int) : a * -b = -(a * b) :=
+  (Int.neg_mul_eq_mul_neg a b).symm
+
+protected theorem neg_mul_neg (a b : Int) : -a * -b = a * b := by simp
+
+protected theorem neg_mul_comm (a b : Int) : -a * b = a * -b := by simp
+
+protected theorem mul_sub (a b c : Int) : a * (b - c) = a * b - a * c := by
+  simp [Int.sub_eq_add_neg, Int.mul_add]
+
+protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
+  simp [Int.sub_eq_add_neg, Int.add_mul]
+
+@[simp] protected theorem one_mul : ∀ a : Int, 1 * a = a
+  | ofNat n => show ofNat (1 * n) = ofNat n by rw [Nat.one_mul]
+  | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]
+
+@[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]
+
+protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]
+
+protected theorem neg_eq_neg_one_mul : ∀ a : Int, -a = -1 * a
+  | 0      => rfl
+  | succ n => show _ = -[1 * n +1] by rw [Nat.one_mul]; rfl
+  | -[n+1] => show _ = ofNat _ by rw [Nat.one_mul]; rfl
+
+protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
+  refine ⟨fun h => ?_, fun h => h.elim (by simp [·, Int.zero_mul]) (by simp [·, Int.mul_zero])⟩
+  exact match a, b, h with
+  | .ofNat 0, _, _ => by simp
+  | _, .ofNat 0, _ => by simp
+  | .ofNat (a+1), .negSucc b, h => by cases h
+
+protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 :=
+  Or.rec a0 b0 ∘ Int.mul_eq_zero.mp
+
+protected theorem eq_of_mul_eq_mul_right {a b c : Int} (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
+  have : (b - c) * a = 0 := by rwa [Int.sub_mul, Int.sub_eq_zero]
+  Int.sub_eq_zero.1 <| (Int.mul_eq_zero.mp this).resolve_right ha
+
+protected theorem eq_of_mul_eq_mul_left {a b c : Int} (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
+  have : a * b - a * c = 0 := Int.sub_eq_zero_of_eq h
+  have : a * (b - c) = 0 := by rw [Int.mul_sub, this]
+  have : b - c = 0 := (Int.mul_eq_zero.1 this).resolve_left ha
+  Int.eq_of_sub_eq_zero this
+
+theorem mul_eq_mul_left_iff {a b c : Int} (h : c ≠ 0) : c * a = c * b ↔ a = b :=
+  ⟨Int.eq_of_mul_eq_mul_left h, fun w => congrArg (fun x => c * x) w⟩
+
+theorem mul_eq_mul_right_iff {a b c : Int} (h : c ≠ 0) : a * c = b * c ↔ a = b :=
+  ⟨Int.eq_of_mul_eq_mul_right h, fun w => congrArg (fun x => x * c) w⟩
+
+theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 :=
+  Int.eq_of_mul_eq_mul_right Hpos <| by rw [Int.one_mul, H]
+
+theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
+  Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
+
+/-! NatCast lemmas -/
+
+/-!
+The following lemmas are later subsumed by e.g. `Nat.cast_add` and `Nat.cast_mul` in Mathlib
+but it is convenient to have these earlier, for users who only need `Nat` and `Int`.
+-/
+
+theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl
+
+theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
+
+@[simp] theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by
+  -- Note this only works because of local simp attributes in this file,
+  -- so it still makes sense to tag the lemmas with `@[simp]`.
+  simp
+
+@[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
+  simp
+
+end Int

src/Init/Data/Int/Order.lean

@@ -0,0 +1,438 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
+-/
+prelude
+import Init.Data.Int.Lemmas
+import Init.ByCases
+
+/-!
+# Results about the order properties of the integers, and the integers as an ordered ring.
+-/
+
+open Nat
+
+namespace Int
+
+/-! ## Order properties of the integers -/
+
+theorem nonneg_def {a : Int} : NonNeg a ↔ ∃ n : Nat, a = n :=
+  ⟨fun ⟨n⟩ => ⟨n, rfl⟩, fun h => match a, h with | _, ⟨n, rfl⟩ => ⟨n⟩⟩
+
+theorem NonNeg.elim {a : Int} : NonNeg a → ∃ n : Nat, a = n := nonneg_def.1
+
+theorem nonneg_or_nonneg_neg : ∀ (a : Int), NonNeg a ∨ NonNeg (-a)
+  | (_:Nat) => .inl ⟨_⟩
+  | -[_+1]  => .inr ⟨_⟩
+
+theorem le_def (a b : Int) : a ≤ b ↔ NonNeg (b - a) := .rfl
+
+theorem lt_iff_add_one_le (a b : Int) : a < b ↔ a + 1 ≤ b := .rfl
+
+theorem le.intro_sub {a b : Int} (n : Nat) (h : b - a = n) : a ≤ b := by
+  simp [le_def, h]; constructor
+
+attribute [local simp] Int.add_left_neg Int.add_right_neg Int.neg_add
+
+theorem le.intro {a b : Int} (n : Nat) (h : a + n = b) : a ≤ b :=
+  le.intro_sub n <| by rw [← h, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]
+
+theorem le.dest_sub {a b : Int} (h : a ≤ b) : ∃ n : Nat, b - a = n := nonneg_def.1 h
+
+theorem le.dest {a b : Int} (h : a ≤ b) : ∃ n : Nat, a + n = b :=
+  let ⟨n, h₁⟩ := le.dest_sub h
+  ⟨n, by rw [← h₁, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]⟩
+
+protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
+  (nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
+    rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
+
+@[simp] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
+  ⟨fun h =>
+    let ⟨k, hk⟩ := le.dest h
+    Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk,
+  fun h =>
+    let ⟨k, (hk : m + k = n)⟩ := Nat.le.dest h
+    le.intro k (by rw [← hk]; rfl)⟩
+
+theorem ofNat_zero_le (n : Nat) : 0 ≤ (↑n : Int) := ofNat_le.2 n.zero_le
+
+theorem eq_ofNat_of_zero_le {a : Int} (h : 0 ≤ a) : ∃ n : Nat, a = n := by
+  have t := le.dest_sub h; rwa [Int.sub_zero] at t
+
+theorem eq_succ_of_zero_lt {a : Int} (h : 0 < a) : ∃ n : Nat, a = n.succ :=
+  let ⟨n, (h : ↑(1 + n) = a)⟩ := le.dest h
+  ⟨n, by rw [Nat.add_comm] at h; exact h.symm⟩
+
+theorem lt_add_succ (a : Int) (n : Nat) : a < a + Nat.succ n :=
+  le.intro n <| by rw [Int.add_comm, Int.add_left_comm]; rfl
+
+theorem lt.intro {a b : Int} {n : Nat} (h : a + Nat.succ n = b) : a < b :=
+  h ▸ lt_add_succ a n
+
+theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b :=
+  let ⟨n, h⟩ := le.dest h; ⟨n, by rwa [Int.add_comm, Int.add_left_comm] at h⟩
+
+@[simp] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by
+  rw [lt_iff_add_one_le, ← ofNat_succ, ofNat_le]; rfl
+
+@[simp] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
+
+theorem ofNat_nonneg (n : Nat) : 0 ≤ (n : Int) := ⟨_⟩
+
+theorem ofNat_succ_pos (n : Nat) : 0 < (succ n : Int) := ofNat_lt.2 <| Nat.succ_pos _
+
+@[simp] protected theorem le_refl (a : Int) : a ≤ a :=
+  le.intro _ (Int.add_zero a)
+
+protected theorem le_trans {a b c : Int} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
+  let ⟨n, hn⟩ := le.dest h₁; let ⟨m, hm⟩ := le.dest h₂
+  le.intro (n + m) <| by rw [← hm, ← hn, Int.add_assoc, ofNat_add]
+
+protected theorem le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b := by
+  let ⟨n, hn⟩ := le.dest h₁; let ⟨m, hm⟩ := le.dest h₂
+  have := hn; rw [← hm, Int.add_assoc, ← ofNat_add] at this
+  have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm
+  rw [← hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]
+
+protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
+  let ⟨n, hn⟩ := lt.dest H
+  have : (a+Nat.succ n) = a+0 := by
+    rw [hn, Int.add_zero]
+  have : Nat.succ n = 0 := Int.ofNat.inj (Int.add_left_cancel this)
+  show False from Nat.succ_ne_zero _ this
+
+protected theorem ne_of_lt {a b : Int} (h : a < b) : a ≠ b := fun e => by
+  cases e; exact Int.lt_irrefl _ h
+
+protected theorem ne_of_gt {a b : Int} (h : b < a) : a ≠ b := (Int.ne_of_lt h).symm
+
+protected theorem le_of_lt {a b : Int} (h : a < b) : a ≤ b :=
+  let ⟨_, hn⟩ := lt.dest h; le.intro _ hn
+
+protected theorem lt_iff_le_and_ne {a b : Int} : a < b ↔ a ≤ b ∧ a ≠ b := by
+  refine ⟨fun h => ⟨Int.le_of_lt h, Int.ne_of_lt h⟩, fun ⟨aleb, aneb⟩ => ?_⟩
+  let ⟨n, hn⟩ := le.dest aleb
+  have : n ≠ 0 := aneb.imp fun eq => by rw [← hn, eq, ofNat_zero, Int.add_zero]
+  apply lt.intro; rwa [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero this)] at hn
+
+theorem lt_succ (a : Int) : a < a + 1 := Int.le_refl _
+
+protected theorem zero_lt_one : (0 : Int) < 1 := ⟨_⟩
+
+protected theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a := by
+  rw [Int.lt_iff_le_and_ne]
+  constructor <;> refine fun ⟨h, h'⟩ => ⟨h, h'.imp fun h' => ?_⟩
+  · exact Int.le_antisymm h h'
+  · subst h'; apply Int.le_refl
+
+protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
+  ⟨fun h => Int.lt_iff_le_not_le.2 ⟨(Int.le_total ..).resolve_right h, h⟩,
+   fun h => (Int.lt_iff_le_not_le.1 h).2⟩
+
+protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
+  by rw [← Int.not_le, Decidable.not_not]
+
+protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=
+  if eq : a = b then .inr <| .inl eq else
+  if le : a ≤ b then .inl <| Int.lt_iff_le_and_ne.2 ⟨le, eq⟩ else
+  .inr <| .inr <| Int.not_le.1 le
+
+protected theorem ne_iff_lt_or_gt {a b : Int} : a ≠ b ↔ a < b ∨ b < a := by
+  constructor
+  · intro h
+    cases Int.lt_trichotomy a b
+    case inl lt => exact Or.inl lt
+    case inr h =>
+      cases h
+      case inl =>simp_all
+      case inr gt => exact Or.inr gt
+  · intro h
+    cases h
+    case inl lt => exact Int.ne_of_lt lt
+    case inr gt => exact Int.ne_of_gt gt
+
+protected theorem lt_or_gt_of_ne {a b : Int} : a ≠ b →  a < b ∨ b < a:= Int.ne_iff_lt_or_gt.mp
+
+protected theorem eq_iff_le_and_ge {x y : Int} : x = y ↔ x ≤ y ∧ y ≤ x := by
+  constructor
+  · simp_all
+  · intro ⟨h₁, h₂⟩
+    exact Int.le_antisymm h₁ h₂
+
+protected theorem lt_of_le_of_lt {a b c : Int} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
+  Int.not_le.1 fun h => Int.not_le.2 h₂ (Int.le_trans h h₁)
+
+protected theorem lt_of_lt_of_le {a b c : Int} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
+  Int.not_le.1 fun h => Int.not_le.2 h₁ (Int.le_trans h₂ h)
+
+protected theorem lt_trans {a b c : Int} (h₁ : a < b) (h₂ : b < c) : a < c :=
+  Int.lt_of_le_of_lt (Int.le_of_lt h₁) h₂
+
+instance : Trans (α := Int) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨Int.le_trans⟩
+
+instance : Trans (α := Int) (· < ·) (· ≤ ·) (· < ·) := ⟨Int.lt_of_lt_of_le⟩
+
+instance : Trans (α := Int) (· ≤ ·) (· < ·) (· < ·) := ⟨Int.lt_of_le_of_lt⟩
+
+instance : Trans (α := Int) (· < ·) (· < ·) (· < ·) := ⟨Int.lt_trans⟩
+
+protected theorem min_def (n m : Int) : min n m = if n ≤ m then n else m := rfl
+
+protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
+
+protected theorem min_comm (a b : Int) : min a b = min b a := by
+  simp [Int.min_def]
+  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
+  · exact Int.le_antisymm h₁ h₂
+  · cases not_or_intro h₁ h₂ <| Int.le_total ..
+
+protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def]; split <;> simp [*]
+
+protected theorem min_le_left (a b : Int) : min a b ≤ a := Int.min_comm .. ▸ Int.min_le_right ..
+
+protected theorem le_min {a b c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
+  ⟨fun h => ⟨Int.le_trans h (Int.min_le_left ..), Int.le_trans h (Int.min_le_right ..)⟩,
+   fun ⟨h₁, h₂⟩ => by rw [Int.min_def]; split <;> assumption⟩
+
+protected theorem max_comm (a b : Int) : max a b = max b a := by
+  simp only [Int.max_def]
+  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
+  · exact Int.le_antisymm h₂ h₁
+  · cases not_or_intro h₁ h₂ <| Int.le_total ..
+
+protected theorem le_max_left (a b : Int) : a ≤ max a b := by rw [Int.max_def]; split <;> simp [*]
+
+protected theorem le_max_right (a b : Int) : b ≤ max a b := Int.max_comm .. ▸ Int.le_max_left ..
+
+protected theorem max_le {a b c : Int} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
+  ⟨fun h => ⟨Int.le_trans (Int.le_max_left ..) h, Int.le_trans (Int.le_max_right ..) h⟩,
+   fun ⟨h₁, h₂⟩ => by rw [Int.max_def]; split <;> assumption⟩
+
+theorem eq_natAbs_of_zero_le {a : Int} (h : 0 ≤ a) : a = natAbs a := by
+  let ⟨n, e⟩ := eq_ofNat_of_zero_le h
+  rw [e]; rfl
+
+theorem le_natAbs {a : Int} : a ≤ natAbs a :=
+  match Int.le_total 0 a with
+  | .inl h => by rw [eq_natAbs_of_zero_le h]; apply Int.le_refl
+  | .inr h => Int.le_trans h (ofNat_zero_le _)
+
+theorem negSucc_lt_zero (n : Nat) : -[n+1] < 0 :=
+  Int.not_le.1 fun h => let ⟨_, h⟩ := eq_ofNat_of_zero_le h; nomatch h
+
+@[simp] theorem negSucc_not_nonneg (n : Nat) : 0 ≤ -[n+1] ↔ False := by
+  simp only [Int.not_le, iff_false]; exact Int.negSucc_lt_zero n
+
+protected theorem add_le_add_left {a b : Int} (h : a ≤ b) (c : Int) : c + a ≤ c + b :=
+  let ⟨n, hn⟩ := le.dest h; le.intro n <| by rw [Int.add_assoc, hn]
+
+protected theorem add_lt_add_left {a b : Int} (h : a < b) (c : Int) : c + a < c + b :=
+  Int.lt_iff_le_and_ne.2 ⟨Int.add_le_add_left (Int.le_of_lt h) _, fun heq =>
+    b.lt_irrefl <| by rwa [Int.add_left_cancel heq] at h⟩
+
+protected theorem add_le_add_right {a b : Int} (h : a ≤ b) (c : Int) : a + c ≤ b + c :=
+  Int.add_comm c a ▸ Int.add_comm c b ▸ Int.add_le_add_left h c
+
+protected theorem add_lt_add_right {a b : Int} (h : a < b) (c : Int) : a + c < b + c :=
+  Int.add_comm c a ▸ Int.add_comm c b ▸ Int.add_lt_add_left h c
+
+protected theorem le_of_add_le_add_left {a b c : Int} (h : a + b ≤ a + c) : b ≤ c := by
+  have : -a + (a + b) ≤ -a + (a + c) := Int.add_le_add_left h _
+  simp [Int.neg_add_cancel_left] at this
+  assumption
+
+protected theorem le_of_add_le_add_right {a b c : Int} (h : a + b ≤ c + b) : a ≤ c :=
+  Int.le_of_add_le_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]
+
+protected theorem add_le_add_iff_left (a : Int) : a + b ≤ a + c ↔ b ≤ c :=
+  ⟨Int.le_of_add_le_add_left, (Int.add_le_add_left · _)⟩
+
+protected theorem add_le_add_iff_right (c : Int) : a + c ≤ b + c ↔ a ≤ b :=
+  ⟨Int.le_of_add_le_add_right, (Int.add_le_add_right · _)⟩
+
+protected theorem add_le_add {a b c d : Int} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
+  Int.le_trans (Int.add_le_add_right h₁ c) (Int.add_le_add_left h₂ b)
+
+protected theorem le_add_of_nonneg_right {a b : Int} (h : 0 ≤ b) : a ≤ a + b := by
+  have : a + b ≥ a + 0 := Int.add_le_add_left h a
+  rwa [Int.add_zero] at this
+
+protected theorem le_add_of_nonneg_left {a b : Int} (h : 0 ≤ b) : a ≤ b + a := by
+  have : 0 + a ≤ b + a := Int.add_le_add_right h a
+  rwa [Int.zero_add] at this
+
+protected theorem neg_le_neg {a b : Int} (h : a ≤ b) : -b ≤ -a := by
+  have : 0 ≤ -a + b := Int.add_left_neg a ▸ Int.add_le_add_left h (-a)
+  have : 0 + -b ≤ -a + b + -b := Int.add_le_add_right this (-b)
+  rwa [Int.add_neg_cancel_right, Int.zero_add] at this
+
+protected theorem le_of_neg_le_neg {a b : Int} (h : -b ≤ -a) : a ≤ b :=
+  suffices - -a ≤ - -b by simp [Int.neg_neg] at this; assumption
+  Int.neg_le_neg h
+
+protected theorem neg_nonpos_of_nonneg {a : Int} (h : 0 ≤ a) : -a ≤ 0 := by
+  have : -a ≤ -0 := Int.neg_le_neg h
+  rwa [Int.neg_zero] at this
+
+protected theorem neg_nonneg_of_nonpos {a : Int} (h : a ≤ 0) : 0 ≤ -a := by
+  have : -0 ≤ -a := Int.neg_le_neg h
+  rwa [Int.neg_zero] at this
+
+protected theorem neg_lt_neg {a b : Int} (h : a < b) : -b < -a := by
+  have : 0 < -a + b := Int.add_left_neg a ▸ Int.add_lt_add_left h (-a)
+  have : 0 + -b < -a + b + -b := Int.add_lt_add_right this (-b)
+  rwa [Int.add_neg_cancel_right, Int.zero_add] at this
+
+protected theorem neg_neg_of_pos {a : Int} (h : 0 < a) : -a < 0 := by
+  have : -a < -0 := Int.neg_lt_neg h
+  rwa [Int.neg_zero] at this
+
+protected theorem neg_pos_of_neg {a : Int} (h : a < 0) : 0 < -a := by
+  have : -0 < -a := Int.neg_lt_neg h
+  rwa [Int.neg_zero] at this
+
+protected theorem sub_nonneg_of_le {a b : Int} (h : b ≤ a) : 0 ≤ a - b := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem le_of_sub_nonneg {a b : Int} (h : 0 ≤ a - b) : b ≤ a := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem sub_pos_of_lt {a b : Int} (h : b < a) : 0 < a - b := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem lt_of_sub_pos {a b : Int} (h : 0 < a - b) : b < a := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem sub_left_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - b ≤ c := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h
+
+protected theorem sub_le_self (a : Int) {b : Int} (h : 0 ≤ b) : a - b ≤ a :=
+  calc  a + -b
+    _ ≤ a + 0 := Int.add_le_add_left (Int.neg_nonpos_of_nonneg h) _
+    _ = a     := by rw [Int.add_zero]
+
+protected theorem sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a :=
+  calc  a + -b
+    _ < a + 0 := Int.add_lt_add_left (Int.neg_neg_of_pos h) _
+    _ = a     := by rw [Int.add_zero]
+
+theorem add_one_le_of_lt {a b : Int} (H : a < b) : a + 1 ≤ b := H
+
+/- ### Order properties and multiplication -/
+
+
+protected theorem mul_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := by
+  let ⟨n, hn⟩ := eq_ofNat_of_zero_le ha
+  let ⟨m, hm⟩ := eq_ofNat_of_zero_le hb
+  rw [hn, hm, ← ofNat_mul]; apply ofNat_nonneg
+
+protected theorem mul_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
+  let ⟨n, hn⟩ := eq_succ_of_zero_lt ha
+  let ⟨m, hm⟩ := eq_succ_of_zero_lt hb
+  rw [hn, hm, ← ofNat_mul]; apply ofNat_succ_pos
+
+protected theorem mul_lt_mul_of_pos_left {a b c : Int}
+  (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b := by
+  have : 0 < c * (b - a) := Int.mul_pos h₂ (Int.sub_pos_of_lt h₁)
+  rw [Int.mul_sub] at this
+  exact Int.lt_of_sub_pos this
+
+protected theorem mul_lt_mul_of_pos_right {a b c : Int}
+  (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c := by
+  have : 0 < b - a := Int.sub_pos_of_lt h₁
+  have : 0 < (b - a) * c := Int.mul_pos this h₂
+  rw [Int.sub_mul] at this
+  exact Int.lt_of_sub_pos this
+
+protected theorem mul_le_mul_of_nonneg_left {a b c : Int}
+    (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
+  if hba : b ≤ a then by
+    rw [Int.le_antisymm hba h₁]; apply Int.le_refl
+  else if hc0 : c ≤ 0 then by
+    simp [Int.le_antisymm hc0 h₂, Int.zero_mul]
+  else by
+    exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
+      (Int.lt_iff_le_not_le.2 ⟨h₁, hba⟩) (Int.lt_iff_le_not_le.2 ⟨h₂, hc0⟩)
+
+protected theorem mul_le_mul_of_nonneg_right {a b c : Int}
+    (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c := by
+  rw [Int.mul_comm, Int.mul_comm b]; exact Int.mul_le_mul_of_nonneg_left h₁ h₂
+
+protected theorem mul_le_mul {a b c d : Int}
+    (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d :=
+  Int.le_trans (Int.mul_le_mul_of_nonneg_right hac nn_b) (Int.mul_le_mul_of_nonneg_left hbd nn_c)
+
+protected theorem mul_nonpos_of_nonneg_of_nonpos {a b : Int}
+  (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0 := by
+  have h : a * b ≤ a * 0 := Int.mul_le_mul_of_nonneg_left hb ha
+  rwa [Int.mul_zero] at h
+
+protected theorem mul_nonpos_of_nonpos_of_nonneg {a b : Int}
+  (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0 := by
+  have h : a * b ≤ 0 * b := Int.mul_le_mul_of_nonneg_right ha hb
+  rwa [Int.zero_mul] at h
+
+protected theorem mul_le_mul_of_nonpos_right {a b c : Int}
+    (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c :=
+  have : -c ≥ 0 := Int.neg_nonneg_of_nonpos hc
+  have : b * -c ≤ a * -c := Int.mul_le_mul_of_nonneg_right h this
+  Int.le_of_neg_le_neg <| by rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this
+
+protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
+    (ha : a ≤ 0) (h : c ≤ b) : a * b ≤ a * c := by
+  rw [Int.mul_comm a b, Int.mul_comm a c]
+  apply Int.mul_le_mul_of_nonpos_right h ha
+
+/- ## natAbs -/
+
+@[simp] theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := rfl
+@[simp] theorem natAbs_negSucc (n : Nat) : natAbs -[n+1] = n.succ := rfl
+@[simp] theorem natAbs_zero : natAbs (0 : Int) = (0 : Nat) := rfl
+@[simp] theorem natAbs_one : natAbs (1 : Int) = (1 : Nat) := rfl
+
+@[simp] theorem natAbs_eq_zero : natAbs a = 0 ↔ a = 0 :=
+  ⟨fun H => match a with
+    | ofNat _ => congrArg ofNat H
+    | -[_+1]  => absurd H (succ_ne_zero _),
+  fun e => e ▸ rfl⟩
+
+theorem natAbs_pos : 0 < natAbs a ↔ a ≠ 0 := by rw [Nat.pos_iff_ne_zero, Ne, natAbs_eq_zero]
+
+@[simp] theorem natAbs_neg : ∀ (a : Int), natAbs (-a) = natAbs a
+  | 0      => rfl
+  | succ _ => rfl
+  | -[_+1] => rfl
+
+theorem natAbs_eq : ∀ (a : Int), a = natAbs a ∨ a = -↑(natAbs a)
+  | ofNat _ => Or.inl rfl
+  | -[_+1]  => Or.inr rfl
+
+theorem natAbs_negOfNat (n : Nat) : natAbs (negOfNat n) = n := by
+  cases n <;> rfl
+
+theorem natAbs_mul (a b : Int) : natAbs (a * b) = natAbs a * natAbs b := by
+  cases a <;> cases b <;>
+    simp only [← Int.mul_def, Int.mul, natAbs_negOfNat] <;> simp only [natAbs]
+
+theorem natAbs_eq_natAbs_iff {a b : Int} : a.natAbs = b.natAbs ↔ a = b ∨ a = -b := by
+  constructor <;> intro h
+  · cases Int.natAbs_eq a with
+    | inl h₁ | inr h₁ =>
+      cases Int.natAbs_eq b with
+      | inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]
+  · cases h with (subst a; try rfl)
+    | inr h => rw [Int.natAbs_neg]
+
+theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
+  match a, eq_ofNat_of_zero_le H with
+  | _, ⟨_, rfl⟩ => rfl
+
+theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
+  rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]

src/Init/Data/Random.lean

@@ -42,17 +42,15 @@ instance : Repr StdGen where
 
 def stdNext : StdGen → Nat × StdGen
   | ⟨s1, s2⟩ =>
-    let s1   : Int := s1
-    let s2   : Int := s2
-    let k    : Int := s1 / 53668
-    let s1'  : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211
-    let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1'
-    let k'   : Int := s2 / 52774
-    let s2'  : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791
-    let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2'
-    let z    : Int := s1'' - s2''
-    let z'   : Int := if z < 1 then z + 2147483562 else z % 2147483562
-    (z'.toNat, ⟨s1''.toNat, s2''.toNat⟩)
+    let k    : Int := Int.ofNat (s1 / 53668)
+    let s1'  : Int := 40014 * (Int.ofNat s1 - k * 53668) - k * 12211
+    let s1'' : Nat := if s1' < 0 then (s1' + 2147483563).toNat else s1'.toNat
+    let k'   : Int := Int.ofNat (s2 / 52774)
+    let s2'  : Int := 40692 * (Int.ofNat s2 - k' * 52774) - k' * 3791
+    let s2'' : Nat := if s2' < 0 then (s2' + 2147483399).toNat else s2'.toNat
+    let z    : Int := Int.ofNat s1'' - Int.ofNat s2''
+    let z'   : Nat := if z < 1 then (z + 2147483562).toNat else z.toNat % 2147483562
+    (z', ⟨s1'', s2''⟩)
 
 def stdSplit : StdGen → StdGen × StdGen
   | g@⟨s1, s2⟩ =>

src/Lean/Data/Json/Basic.lean

@@ -98,7 +98,7 @@ protected def toString : JsonNumber → String
     -- grow exponentially in the value of exponent.
     let exp : Int := 9 + countDigits m - (e : Int)
     let exp := if exp < 0 then exp else 0
-    let e' := (10 : Int) ^ (e - exp.natAbs)
+    let e' := 10 ^ (e - exp.natAbs)
     let left := (m / e').repr
     if m % e' = 0 && exp = 0 then
       s!"{sign}{left}"

src/Lean/Data/Rat.lean

@@ -24,7 +24,7 @@ instance : Repr Rat where
 
 @[inline] def Rat.normalize (a : Rat) : Rat :=
   let n := Nat.gcd a.num.natAbs a.den
-  if n == 1 then a else { num := a.num / n, den := a.den / n }
+  if n == 1 then a else { num := a.num.div n, den := a.den / n }
 
 def mkRat (num : Int) (den : Nat) : Rat :=
   if den == 0 then { num := 0 } else Rat.normalize { num, den }
@@ -48,7 +48,7 @@ protected def lt (a b : Rat) : Bool :=
 protected def mul (a b : Rat) : Rat :=
   let g1 := Nat.gcd a.den b.num.natAbs
   let g2 := Nat.gcd a.num.natAbs b.den
-  { num := (a.num / g2)*(b.num / g1)
+  { num := (a.num.div g2)*(b.num.div g1)
     den := (b.den / g2)*(a.den / g1) }
 
 protected def inv (a : Rat) : Rat :=
@@ -68,12 +68,12 @@ protected def add (a b : Rat) : Rat :=
     { num := a.num * b.den + b.num * a.den, den := a.den * b.den }
   else
     let den := (a.den / g) * b.den
-    let num := (b.den / g) * a.num + (a.den / g) * b.num
+    let num := Int.ofNat (b.den / g) * a.num + Int.ofNat (a.den / g) * b.num
     let g1  := Nat.gcd num.natAbs g
     if g1 == 1 then
       { num, den }
     else
-      { num := num / g1, den := den / g1 }
+      { num := num.div g1, den := den / g1 }
 
 protected def sub (a b : Rat) : Rat :=
   let g := Nat.gcd a.den b.den
@@ -86,7 +86,7 @@ protected def sub (a b : Rat) : Rat :=
     if g1 == 1 then
       { num, den }
     else
-      { num := num / g1, den := den / g1 }
+      { num := num.div g1, den := den / g1 }
 
 protected def neg (a : Rat) : Rat :=
   { a with num := - a.num }
@@ -95,14 +95,14 @@ protected def floor (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num / a.den
+    let r := a.num.mod a.den
     if a.num < 0 then r - 1 else r
 
 protected def ceil (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num / a.den
+    let r := a.num.mod a.den
     if a.num > 0 then r + 1 else r
 
 instance : LT Rat where

src/Lean/ToExpr.lean

@@ -28,6 +28,12 @@ instance : ToExpr Nat where
   toExpr     := mkNatLit
   toTypeExpr := mkConst ``Nat
 
+instance : ToExpr Int where
+  toTypeExpr := .const ``Int []
+  toExpr i := match i with
+    | .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
+    | .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)
+
 instance : ToExpr Bool where
   toExpr     := fun b => if b then mkConst ``Bool.true else mkConst ``Bool.false
   toTypeExpr := mkConst ``Bool

tests/lean/binopIssues.lean

@@ -1,5 +1,3 @@
-axiom Int.add_comm (i j : Int) : i + j = j + i
-
 example (n : Nat) (i : Int) : n + i = i + n := by
   rw [Int.add_comm]
 

tests/lean/matchOfNatIssue.lean.expected.out

@@ -1,3 +1,3 @@
 x : Int
 h : x = 2
-⊢ Int.ofNat 2 = x
+⊢ 2 = x

tests/lean/run/inaccessibleAnnotDefEqIssue.lean

@@ -2,7 +2,7 @@ example : Int → Nat
 | (_ : Nat)     => 0
 | Int.negSucc n => 0
 
-protected theorem Int.add_comm : ∀ a b : Int, a + b = b + a
+protected theorem Int.add_comm' : ∀ a b : Int, a + b = b + a
 | (n : Nat), (m : Nat)         => sorry
 | (_ : Nat), Int.negSucc _     => rfl
 | Int.negSucc _, (_ : Nat)     => rfl

tests/lean/run/mathlibetaissue.lean

@@ -27,11 +27,6 @@ Section titles correspond to the files the material came from the mathlib4/std4.
 
 section Std.Data.Int.Lemmas
 
-namespace Int
-theorem add_zero : ∀ a : Int, a + 0 = a := sorry
-theorem mul_one (a : Int) : a * 1 = a := sorry
-end Int
-
 end Std.Data.Int.Lemmas
 
 section Std.Classes.RatCast