chore: upstream gcd/lcm lemmas

src/Init/Data/BitVec/Basic.lean

@@ -73,6 +73,9 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
+@[deprecated isLt]
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
+
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

src/Init/Data/BitVec/Lemmas.lean

@@ -29,8 +29,6 @@ theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
 @[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
-theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
-
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
 
 @[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
@@ -458,12 +456,12 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   | y+1 =>
     rw [Nat.succ_eq_add_one] at h
     rw [← h]
-    rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
+    rw [Nat.testBit_two_pow_sub_succ (isLt _)]
     · cases w : decide (i < v)
       · simp at w
         simp [w]
         rw [Nat.testBit_lt_two_pow]
-        calc BitVec.toNat x < 2 ^ v := toNat_lt _
+        calc BitVec.toNat x < 2 ^ v := isLt _
           _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
       · simp
 
@@ -520,7 +518,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
   · simp
     rw [Nat.mod_eq_of_lt]
     rw [Nat.shiftLeft_eq, Nat.pow_add]
-    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
+    exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
   · omega
 
 @[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :

src/Init/Data/Int.lean

@@ -11,3 +11,4 @@ import Init.Data.Int.DivModLemmas
 import Init.Data.Int.Gcd
 import Init.Data.Int.Lemmas
 import Init.Data.Int.Order
+import Init.Data.Int.Pow

src/Init/Data/Int/DivMod.lean

@@ -160,6 +160,12 @@ instance : Mod Int where
 
 @[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
+theorem ofNat_div (m n : Nat) : ↑(m / n) = div ↑m ↑n := rfl
+
+theorem ofNat_fdiv : ∀ m n : Nat, ↑(m / n) = fdiv ↑m ↑n
+  | 0, _ => by simp [fdiv]
+  | succ _, _ => rfl
+
 /-!
 # `bmod` ("balanced" mod)
 

src/Init/Data/Int/Gcd.lean

@@ -6,7 +6,12 @@ Authors: Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Data.Nat.Gcd
+import Init.Data.Nat.Lcm
+import Init.Data.Int.DivModLemmas
 
+/-!
+Definition and lemmas for gcd and lcm over Int
+-/
 namespace Int
 
 /-! ## gcd -/
@@ -14,4 +19,37 @@ namespace Int
 /-- Computes the greatest common divisor of two integers, as a `Nat`. -/
 def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs
 
+theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a := by
+  have := Nat.gcd_dvd_left a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b := by
+  have := Nat.gcd_dvd_right a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]
+@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]
+
+@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]
+@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]
+
+/-! ## lcm -/
+
+/-- Computes the least common multiple of two integers, as a `Nat`. -/
+def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  simp only [lcm]
+  apply Nat.lcm_ne_zero <;> simpa
+
+theorem dvd_lcm_left {a b : Int} : a ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))
+
+theorem dvd_lcm_right {a b : Int} : b ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))
+
+@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _
+
 end Int

src/Init/Data/Int/Lemmas.lean

@@ -499,33 +499,6 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
 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]
 
-/-! # pow -/
-
-protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
-
-protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
-protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
-  rw [Int.mul_comm, Int.pow_succ]
-
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
-  | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
-
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
-  | 0,      h =>
-    have : i = 0 := eq_zero_of_le_zero h
-    this.symm ▸ Nat.le_refl _
-  | succ j, h =>
-    match le_or_eq_of_le_succ h with
-    | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
-      Nat.mul_one (n^i) ▸ this
-    | Or.inr h =>
-      h.symm ▸ Nat.le_refl _
-
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
-
 /-! NatCast lemmas -/
 
 /-!
@@ -545,10 +518,4 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 @[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
   simp
 
-theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
-  match n with
-  | 0 => rfl
-  | n + 1 =>
-    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
-
 end Int

src/Init/Data/Int/Order.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Lemmas
 import Init.ByCases
+import Init.RCases
 
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
@@ -498,3 +499,524 @@ theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toN
 @[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
   | 0 => rfl
   | _+1 => rfl
+
+/-! ### toNat' -/
+
+theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
+  | (m : Nat), n => by simp [toNat', Int.ofNat_inj]
+  | -[m+1], n => by constructor <;> nofun
+
+/-! ## Order properties of the integers -/
+
+protected theorem lt_of_not_ge {a b : Int} : ¬a ≤ b → b < a := Int.not_le.mp
+protected theorem not_le_of_gt {a b : Int} : b < a → ¬a ≤ b := Int.not_le.mpr
+
+protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
+
+@[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False := by
+  simp only [Int.not_lt, iff_false]; constructor
+
+theorem eq_negSucc_of_lt_zero : ∀ {a : Int}, a < 0 → ∃ n : Nat, a = -[n+1]
+  | ofNat _, h => absurd h (Int.not_lt.2 (ofNat_zero_le _))
+  | -[n+1],  _ => ⟨n, rfl⟩
+
+protected theorem lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c := by
+  have : -a + (a + b) < -a + (a + c) := Int.add_lt_add_left h _
+  simp [Int.neg_add_cancel_left] at this
+  assumption
+
+protected theorem lt_of_add_lt_add_right {a b c : Int} (h : a + b < c + b) : a < c :=
+  Int.lt_of_add_lt_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]
+
+protected theorem add_lt_add_iff_left (a : Int) : a + b < a + c ↔ b < c :=
+  ⟨Int.lt_of_add_lt_add_left, (Int.add_lt_add_left · _)⟩
+
+protected theorem add_lt_add_iff_right (c : Int) : a + c < b + c ↔ a < b :=
+  ⟨Int.lt_of_add_lt_add_right, (Int.add_lt_add_right · _)⟩
+
+protected theorem add_lt_add {a b c d : Int} (h₁ : a < b) (h₂ : c < d) : a + c < b + d :=
+  Int.lt_trans (Int.add_lt_add_right h₁ c) (Int.add_lt_add_left h₂ b)
+
+protected theorem add_lt_add_of_le_of_lt {a b c d : Int} (h₁ : a ≤ b) (h₂ : c < d) :
+    a + c < b + d :=
+  Int.lt_of_le_of_lt (Int.add_le_add_right h₁ c) (Int.add_lt_add_left h₂ b)
+
+protected theorem add_lt_add_of_lt_of_le {a b c d : Int} (h₁ : a < b) (h₂ : c ≤ d) :
+    a + c < b + d :=
+  Int.lt_of_lt_of_le (Int.add_lt_add_right h₁ c) (Int.add_le_add_left h₂ b)
+
+protected theorem lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b := by
+  have : a + 0 < a + b := Int.add_lt_add_left h a
+  rwa [Int.add_zero] at this
+
+protected theorem lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a := by
+  have : 0 + a < b + a := Int.add_lt_add_right h a
+  rwa [Int.zero_add] at this
+
+protected theorem add_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
+  Int.zero_add 0 ▸ Int.add_le_add ha hb
+
+protected theorem add_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add ha hb
+
+protected theorem add_pos_of_pos_of_nonneg {a b : Int} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_lt_of_le ha hb
+
+protected theorem add_pos_of_nonneg_of_pos {a b : Int} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_le_of_lt ha hb
+
+protected theorem add_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
+  Int.zero_add 0 ▸ Int.add_le_add ha hb
+
+protected theorem add_neg {a b : Int} (ha : a < 0) (hb : b < 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add ha hb
+
+protected theorem add_neg_of_neg_of_nonpos {a b : Int} (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_lt_of_le ha hb
+
+protected theorem add_neg_of_nonpos_of_neg {a b : Int} (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
+  Int.zero_add 0 ▸ Int.add_lt_add_of_le_of_lt ha hb
+
+protected theorem lt_add_of_le_of_pos {a b c : Int} (hbc : b ≤ c) (ha : 0 < a) : b < c + a :=
+  Int.add_zero b ▸ Int.add_lt_add_of_le_of_lt hbc ha
+
+theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
+
+theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
+
+@[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
+  lt_add_one_iff.2 (ofNat_zero_le _)
+
+theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
+  Int.le_of_lt (Int.lt_add_one_iff.2 h)
+
+protected theorem nonneg_of_neg_nonpos {a : Int} (h : -a ≤ 0) : 0 ≤ a :=
+  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
+
+protected theorem nonpos_of_neg_nonneg {a : Int} (h : 0 ≤ -a) : a ≤ 0 :=
+  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]
+
+protected theorem lt_of_neg_lt_neg {a b : Int} (h : -b < -a) : a < b :=
+  Int.neg_neg a ▸ Int.neg_neg b ▸ Int.neg_lt_neg h
+
+protected theorem pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a :=
+  Int.lt_of_neg_lt_neg <| by rwa [Int.neg_zero]
+
+protected theorem neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0 :=
+  have : -0 < -a := by rwa [Int.neg_zero]
+  Int.lt_of_neg_lt_neg this
+
+protected theorem le_neg_of_le_neg {a b : Int} (h : a ≤ -b) : b ≤ -a := by
+  have h := Int.neg_le_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem neg_le_of_neg_le {a b : Int} (h : -a ≤ b) : -b ≤ a := by
+  have h := Int.neg_le_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem lt_neg_of_lt_neg {a b : Int} (h : a < -b) : b < -a := by
+  have h := Int.neg_lt_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem neg_lt_of_neg_lt {a b : Int} (h : -a < b) : -b < a := by
+  have h := Int.neg_lt_neg h
+  rwa [Int.neg_neg] at h
+
+protected theorem sub_nonpos_of_le {a b : Int} (h : a ≤ b) : a - b ≤ 0 := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem le_of_sub_nonpos {a b : Int} (h : a - b ≤ 0) : a ≤ b := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem sub_neg_of_lt {a b : Int} (h : a < b) : a - b < 0 := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_right_neg] at h
+
+protected theorem lt_of_sub_neg {a b : Int} (h : a - b < 0) : a < b := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel, Int.zero_add] at h
+
+protected theorem add_le_of_le_neg_add {a b c : Int} (h : b ≤ -a + c) : a + b ≤ c := by
+  have h := Int.add_le_add_left h a
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem le_neg_add_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ -a + c := by
+  have h := Int.add_le_add_left h (-a)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem add_le_of_le_sub_left {a b c : Int} (h : b ≤ c - a) : a + b ≤ c := by
+  have h := Int.add_le_add_left h a
+  rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
+
+protected theorem le_sub_left_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ c - a := by
+  have h := Int.add_le_add_right h (-a)
+  rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
+
+protected theorem add_le_of_le_sub_right {a b c : Int} (h : a ≤ c - b) : a + b ≤ c := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem le_sub_right_of_add_le {a b c : Int} (h : a + b ≤ c) : a ≤ c - b := by
+  have h := Int.add_le_add_right h (-b)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem le_add_of_neg_add_le {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c := by
+  have h := Int.add_le_add_left h b
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem neg_add_le_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c := by
+  have h := Int.add_le_add_left h (-b)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem le_add_of_sub_left_le {a b c : Int} (h : a - b ≤ c) : a ≤ b + c := by
+  have h := Int.add_le_add_right h b
+  rwa [Int.sub_add_cancel, Int.add_comm] at h
+
+protected theorem le_add_of_sub_right_le {a b c : Int} (h : a - c ≤ b) : a ≤ b + c := by
+  have h := Int.add_le_add_right h c
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem sub_right_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - c ≤ b := by
+  have h := Int.add_le_add_right h (-c)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem le_add_of_neg_add_le_left {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c := by
+  rw [Int.add_comm] at h
+  exact Int.le_add_of_sub_left_le h
+
+protected theorem neg_add_le_left_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c := by
+  rw [Int.add_comm]
+  exact Int.sub_left_le_of_le_add h
+
+protected theorem le_add_of_neg_add_le_right {a b c : Int} (h : -c + a ≤ b) : a ≤ b + c := by
+  rw [Int.add_comm] at h
+  exact Int.le_add_of_sub_right_le h
+
+protected theorem neg_add_le_right_of_le_add {a b c : Int} (h : a ≤ b + c) : -c + a ≤ b := by
+  rw [Int.add_comm] at h
+  exact Int.neg_add_le_left_of_le_add h
+
+protected theorem le_add_of_neg_le_sub_left {a b c : Int} (h : -a ≤ b - c) : c ≤ a + b :=
+  Int.le_add_of_neg_add_le_left (Int.add_le_of_le_sub_right h)
+
+protected theorem neg_le_sub_left_of_le_add {a b c : Int} (h : c ≤ a + b) : -a ≤ b - c := by
+  have h := Int.le_neg_add_of_add_le (Int.sub_left_le_of_le_add h)
+  rwa [Int.add_comm] at h
+
+protected theorem le_add_of_neg_le_sub_right {a b c : Int} (h : -b ≤ a - c) : c ≤ a + b :=
+  Int.le_add_of_sub_right_le (Int.add_le_of_le_sub_left h)
+
+protected theorem neg_le_sub_right_of_le_add {a b c : Int} (h : c ≤ a + b) : -b ≤ a - c :=
+  Int.le_sub_left_of_add_le (Int.sub_right_le_of_le_add h)
+
+protected theorem sub_le_of_sub_le {a b c : Int} (h : a - b ≤ c) : a - c ≤ b :=
+  Int.sub_left_le_of_le_add (Int.le_add_of_sub_right_le h)
+
+protected theorem sub_le_sub_left {a b : Int} (h : a ≤ b) (c : Int) : c - b ≤ c - a :=
+  Int.add_le_add_left (Int.neg_le_neg h) c
+
+protected theorem sub_le_sub_right {a b : Int} (h : a ≤ b) (c : Int) : a - c ≤ b - c :=
+  Int.add_le_add_right h (-c)
+
+protected theorem sub_le_sub {a b c d : Int} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
+  Int.add_le_add hab (Int.neg_le_neg hcd)
+
+protected theorem add_lt_of_lt_neg_add {a b c : Int} (h : b < -a + c) : a + b < c := by
+  have h := Int.add_lt_add_left h a
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem lt_neg_add_of_add_lt {a b c : Int} (h : a + b < c) : b < -a + c := by
+  have h := Int.add_lt_add_left h (-a)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem add_lt_of_lt_sub_left {a b c : Int} (h : b < c - a) : a + b < c := by
+  have h := Int.add_lt_add_left h a
+  rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h
+
+protected theorem lt_sub_left_of_add_lt {a b c : Int} (h : a + b < c) : b < c - a := by
+  have h := Int.add_lt_add_right h (-a)
+  rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h
+
+protected theorem add_lt_of_lt_sub_right {a b c : Int} (h : a < c - b) : a + b < c := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c - b := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c := by
+  have h := Int.add_lt_add_left h b
+  rwa [Int.add_neg_cancel_left] at h
+
+protected theorem neg_add_lt_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
+  have h := Int.add_lt_add_left h (-b)
+  rwa [Int.neg_add_cancel_left] at h
+
+protected theorem lt_add_of_sub_left_lt {a b c : Int} (h : a - b < c) : a < b + c := by
+  have h := Int.add_lt_add_right h b
+  rwa [Int.sub_add_cancel, Int.add_comm] at h
+
+protected theorem sub_left_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - b < c := by
+  have h := Int.add_lt_add_right h (-b)
+  rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_sub_right_lt {a b c : Int} (h : a - c < b) : a < b + c := by
+  have h := Int.add_lt_add_right h c
+  rwa [Int.sub_add_cancel] at h
+
+protected theorem sub_right_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - c < b := by
+  have h := Int.add_lt_add_right h (-c)
+  rwa [Int.add_neg_cancel_right] at h
+
+protected theorem lt_add_of_neg_add_lt_left {a b c : Int} (h : -b + a < c) : a < b + c := by
+  rw [Int.add_comm] at h
+  exact Int.lt_add_of_sub_left_lt h
+
+protected theorem neg_add_lt_left_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c := by
+  rw [Int.add_comm]
+  exact Int.sub_left_lt_of_lt_add h
+
+protected theorem lt_add_of_neg_add_lt_right {a b c : Int} (h : -c + a < b) : a < b + c := by
+  rw [Int.add_comm] at h
+  exact Int.lt_add_of_sub_right_lt h
+
+protected theorem neg_add_lt_right_of_lt_add {a b c : Int} (h : a < b + c) : -c + a < b := by
+  rw [Int.add_comm] at h
+  exact Int.neg_add_lt_left_of_lt_add h
+
+protected theorem lt_add_of_neg_lt_sub_left {a b c : Int} (h : -a < b - c) : c < a + b :=
+  Int.lt_add_of_neg_add_lt_left (Int.add_lt_of_lt_sub_right h)
+
+protected theorem neg_lt_sub_left_of_lt_add {a b c : Int} (h : c < a + b) : -a < b - c := by
+  have h := Int.lt_neg_add_of_add_lt (Int.sub_left_lt_of_lt_add h)
+  rwa [Int.add_comm] at h
+
+protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c < a + b :=
+  Int.lt_add_of_sub_right_lt (Int.add_lt_of_lt_sub_left h)
+
+protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
+  Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
+
+protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
+  Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
+
+protected theorem sub_lt_sub_left {a b : Int} (h : a < b) (c : Int) : c - b < c - a :=
+  Int.add_lt_add_left (Int.neg_lt_neg h) c
+
+protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b - c :=
+  Int.add_lt_add_right h (-c)
+
+protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
+  Int.add_lt_add hab (Int.neg_lt_neg hcd)
+
+protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
+  (hab : a ≤ b) (hcd : c < d) : a - d < b - c :=
+  Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)
+
+protected theorem sub_lt_sub_of_lt_of_le {a b c d : Int}
+  (hab : a < b) (hcd : c ≤ d) : a - d < b - c :=
+  Int.add_lt_add_of_lt_of_le hab (Int.neg_le_neg hcd)
+
+protected theorem add_le_add_three {a b c d e f : Int}
+    (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f :=
+  Int.add_le_add (Int.add_le_add h₁ h₂) h₃
+
+theorem exists_eq_neg_ofNat {a : Int} (H : a ≤ 0) : ∃ n : Nat, a = -(n : Int) :=
+  let ⟨n, h⟩ := eq_ofNat_of_zero_le (Int.neg_nonneg_of_nonpos H)
+  ⟨n, Int.eq_neg_of_eq_neg h.symm⟩
+
+theorem lt_of_add_one_le {a b : Int} (H : a + 1 ≤ b) : a < b := H
+
+theorem lt_add_one_of_le {a b : Int} (H : a ≤ b) : a < b + 1 := Int.add_le_add_right H 1
+
+theorem le_of_lt_add_one {a b : Int} (H : a < b + 1) : a ≤ b := Int.le_of_add_le_add_right H
+
+theorem sub_one_lt_of_le {a b : Int} (H : a ≤ b) : a - 1 < b :=
+  Int.sub_right_lt_of_lt_add <| lt_add_one_of_le H
+
+theorem le_of_sub_one_lt {a b : Int} (H : a - 1 < b) : a ≤ b :=
+  le_of_lt_add_one <| Int.lt_add_of_sub_right_lt H
+
+theorem le_sub_one_of_lt {a b : Int} (H : a < b) : a ≤ b - 1 := Int.le_sub_right_of_add_le H
+
+theorem lt_of_le_sub_one {a b : Int} (H : a ≤ b - 1) : a < b := Int.add_le_of_le_sub_right H
+
+/- ### Order properties and multiplication -/
+
+protected theorem mul_lt_mul {a b c d : Int}
+    (h₁ : a < c) (h₂ : b ≤ d) (h₃ : 0 < b) (h₄ : 0 ≤ c) : a * b < c * d :=
+  Int.lt_of_lt_of_le (Int.mul_lt_mul_of_pos_right h₁ h₃) (Int.mul_le_mul_of_nonneg_left h₂ h₄)
+
+protected theorem mul_lt_mul' {a b c d : Int}
+    (h₁ : a ≤ c) (h₂ : b < d) (h₃ : 0 ≤ b) (h₄ : 0 < c) : a * b < c * d :=
+  Int.lt_of_le_of_lt (Int.mul_le_mul_of_nonneg_right h₁ h₃) (Int.mul_lt_mul_of_pos_left h₂ h₄)
+
+protected theorem mul_neg_of_pos_of_neg {a b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0 := by
+  have h : a * b < a * 0 := Int.mul_lt_mul_of_pos_left hb ha
+  rwa [Int.mul_zero] at h
+
+protected theorem mul_neg_of_neg_of_pos {a b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0 := by
+  have h : a * b < 0 * b := Int.mul_lt_mul_of_pos_right ha hb
+  rwa [Int.zero_mul] at h
+
+protected theorem mul_nonneg_of_nonpos_of_nonpos {a b : Int}
+  (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b := by
+  have : 0 * b ≤ a * b := Int.mul_le_mul_of_nonpos_right ha hb
+  rwa [Int.zero_mul] at this
+
+protected theorem mul_lt_mul_of_neg_left {a b c : Int} (h : b < a) (hc : c < 0) : c * a < c * b :=
+  have : -c > 0 := Int.neg_pos_of_neg hc
+  have : -c * b < -c * a := Int.mul_lt_mul_of_pos_left h this
+  have : -(c * b) < -(c * a) := by
+    rwa [← Int.neg_mul_eq_neg_mul, ← Int.neg_mul_eq_neg_mul] at this
+  Int.lt_of_neg_lt_neg this
+
+protected theorem mul_lt_mul_of_neg_right {a b c : Int} (h : b < a) (hc : c < 0) : a * c < b * c :=
+  have : -c > 0 := Int.neg_pos_of_neg hc
+  have : b * -c < a * -c := Int.mul_lt_mul_of_pos_right h this
+  have : -(b * c) < -(a * c) := by
+    rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this
+  Int.lt_of_neg_lt_neg this
+
+protected theorem mul_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b := by
+  have : 0 * b < a * b := Int.mul_lt_mul_of_neg_right ha hb
+  rwa [Int.zero_mul] at this
+
+protected theorem mul_self_le_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b :=
+  Int.mul_le_mul h2 h2 h1 (Int.le_trans h1 h2)
+
+protected theorem mul_self_lt_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
+  Int.mul_lt_mul' (Int.le_of_lt h2) h2 h1 (Int.lt_of_le_of_lt h1 h2)
+
+/- ## sign -/
+
+@[simp] theorem sign_zero : sign 0 = 0 := rfl
+@[simp] theorem sign_one : sign 1 = 1 := rfl
+theorem sign_neg_one : sign (-1) = -1 := rfl
+
+@[simp] theorem sign_of_add_one (x : Nat) : Int.sign (x + 1) = 1 := rfl
+@[simp] theorem sign_negSucc (x : Nat) : Int.sign (Int.negSucc x) = -1 := rfl
+
+theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
+  match z with | 0 | succ _ | -[_+1] => rfl
+
+theorem natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1 := by
+  rw [Int.natAbs_sign, if_neg hz]
+
+theorem sign_ofNat_of_nonzero {n : Nat} (hn : n ≠ 0) : Int.sign n = 1 :=
+  match n, Nat.exists_eq_succ_of_ne_zero hn with
+  | _, ⟨n, rfl⟩ => Int.sign_of_add_one n
+
+@[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
+  match z with | 0 | succ _ | -[_+1] => rfl
+
+theorem sign_mul_natAbs : ∀ a : Int, sign a * natAbs a = a
+  | 0      => rfl
+  | succ _ => Int.one_mul _
+  | -[_+1] => (Int.neg_eq_neg_one_mul _).symm
+
+@[simp] theorem sign_mul : ∀ a b, sign (a * b) = sign a * sign b
+  | a, 0 | 0, b => by simp [Int.mul_zero, Int.zero_mul]
+  | succ _, succ _ | succ _, -[_+1] | -[_+1], succ _ | -[_+1], -[_+1] => rfl
+
+theorem sign_eq_one_of_pos {a : Int} (h : 0 < a) : sign a = 1 :=
+  match a, eq_succ_of_zero_lt h with
+  | _, ⟨_, rfl⟩ => rfl
+
+theorem sign_eq_neg_one_of_neg {a : Int} (h : a < 0) : sign a = -1 :=
+  match a, eq_negSucc_of_lt_zero h with
+  | _, ⟨_, rfl⟩ => rfl
+
+theorem eq_zero_of_sign_eq_zero : ∀ {a : Int}, sign a = 0 → a = 0
+  | 0, _ => rfl
+
+theorem pos_of_sign_eq_one : ∀ {a : Int}, sign a = 1 → 0 < a
+  | (_ + 1 : Nat), _ => ofNat_lt.2 (Nat.succ_pos _)
+
+theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
+  | (_ + 1 : Nat), h => nomatch h
+  | 0, h => nomatch h
+  | -[_+1], _ => negSucc_lt_zero _
+
+theorem sign_eq_one_iff_pos (a : Int) : sign a = 1 ↔ 0 < a :=
+  ⟨pos_of_sign_eq_one, sign_eq_one_of_pos⟩
+
+theorem sign_eq_neg_one_iff_neg (a : Int) : sign a = -1 ↔ a < 0 :=
+  ⟨neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg⟩
+
+@[simp] theorem sign_eq_zero_iff_zero (a : Int) : sign a = 0 ↔ a = 0 :=
+  ⟨eq_zero_of_sign_eq_zero, fun h => by rw [h, sign_zero]⟩
+
+@[simp] theorem sign_sign : sign (sign x) = sign x := by
+  match x with
+  | 0 => rfl
+  | .ofNat (_ + 1) => rfl
+  | .negSucc _ => rfl
+
+@[simp] theorem sign_nonneg : 0 ≤ sign x ↔ 0 ≤ x := by
+  match x with
+  | 0 => rfl
+  | .ofNat (_ + 1) =>
+    simp (config := { decide := true }) only [sign, true_iff]
+    exact Int.le_add_one (ofNat_nonneg _)
+  | .negSucc _ => simp (config := { decide := true }) [sign]
+
+theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
+  | succ _ => Int.mul_one _
+  | 0 => Int.mul_zero _
+  | -[_+1] => Int.mul_neg_one _
+
+/- ## natAbs -/
+
+theorem natAbs_ne_zero {a : Int} : a.natAbs ≠ 0 ↔ a ≠ 0 := not_congr Int.natAbs_eq_zero
+
+theorem natAbs_mul_self : ∀ {a : Int}, ↑(natAbs a * natAbs a) = a * a
+  | ofNat _ => rfl
+  | -[_+1]  => rfl
+
+theorem eq_nat_or_neg (a : Int) : ∃ n : Nat, a = n ∨ a = -↑n := ⟨_, natAbs_eq a⟩
+
+theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat}
+    (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs]
+
+@[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by
+  rw [← Int.ofNat_mul, natAbs_mul_self]
+
+theorem natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = n ∨ a = -↑n := by
+  rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_ofNat]
+
+theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by
+  suffices ∀ a b : Nat, natAbs (subNatNat a b.succ) ≤ (a + b).succ by
+    match a, b with
+    | (a:Nat), (b:Nat) => rw [ofNat_add_ofNat, natAbs_ofNat]; apply Nat.le_refl
+    | (a:Nat), -[b+1]  => rw [natAbs_ofNat, natAbs_negSucc]; apply this
+    | -[a+1],  (b:Nat) =>
+      rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]; apply this
+    | -[a+1],  -[b+1]  => rw [natAbs_negSucc, succ_add]; apply Nat.le_refl
+  refine fun a b => subNatNat_elim a b.succ
+    (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
+    (fun i n (e : (n + i).succ = _) => ?_) rfl
+  · rintro i n rfl
+    rw [Nat.add_comm _ i, Nat.add_assoc]
+    exact Nat.le_add_right i (b.succ + b).succ
+  · apply succ_le_succ
+    rw [← succ.inj e, ← Nat.add_assoc, Nat.add_comm]
+    apply Nat.le_add_right
+
+theorem natAbs_sub_le (a b : Int) : natAbs (a - b) ≤ natAbs a + natAbs b := by
+  rw [← Int.natAbs_neg b]; apply natAbs_add_le
+
+theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1 := by simp only [negSucc_eq, Int.neg_add]; rfl
+
+theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
+    (w₁ : 0 ≤ a) (w₂ : a < b) : a.natAbs < b.natAbs :=
+  match a, b, eq_ofNat_of_zero_le w₁, eq_ofNat_of_zero_le (Int.le_trans w₁ (Int.le_of_lt w₂)) with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_lt.1 w₂
+
+theorem eq_natAbs_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0 := by
+  rw [natAbs_eq_iff, Int.mul_eq_zero, ← Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
+
+end Int

src/Init/Data/Int/Pow.lean

@@ -0,0 +1,44 @@
+/-
+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
+
+namespace Int
+
+/-! # pow -/
+
+protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
+
+protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
+protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
+  rw [Int.mul_comm, Int.pow_succ]
+
+theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
+  | 0      => Nat.le_refl _
+  | i + 1 => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
+
+theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
+  | 0,      h =>
+    have : i = 0 := Nat.eq_zero_of_le_zero h
+    this.symm ▸ Nat.le_refl _
+  | j + 1, h =>
+    match Nat.le_or_eq_of_le_succ h with
+    | Or.inl h => show n^i ≤ n^j * n from
+      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
+      Nat.mul_one (n^i) ▸ this
+    | Or.inr h =>
+      h.symm ▸ Nat.le_refl _
+
+theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
+  pow_le_pow_of_le_right h (Nat.zero_le _)
+
+theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
+  match n with
+  | 0 => rfl
+  | n + 1 =>
+    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
+
+end Int

src/Init/Data/Nat/Basic.lean

@@ -232,6 +232,9 @@ protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
 protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
   rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
 
+protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
+protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
+
 /-! # Inequalities -/
 
 attribute [simp] Nat.le_refl

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

@@ -6,6 +6,7 @@ Authors: Joe Hendrix
 
 prelude
 import Init.Data.Bool
+import Init.Data.Int.Pow
 import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.TacticsExtra

src/Init/Data/Nat/Div.lean

@@ -10,6 +10,13 @@ import Init.Data.Nat.Basic
 
 namespace Nat
 
+/--
+Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
+there is some `c` such that `b = a * c`.
+-/
+instance : Dvd Nat where
+  dvd a b := Exists (fun c => b = a * c)
+
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
   fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
 

src/Init/Data/Nat/Dvd.lean

@@ -5,17 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
-import Init.TacticsExtra
+import Init.Meta
 
 namespace Nat
 
-/--
-Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
-there is some `c` such that `b = a * c`.
--/
-instance : Dvd Nat where
-  dvd a b := Exists (fun c => b = a * c)
-
 protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
 
 protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩

src/Init/Data/Nat/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Dvd
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
@@ -410,10 +409,6 @@ protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
 protected theorem mul_mul_mul_comm (a b c d : Nat) : (a * b) * (c * d) = (a * c) * (b * d) := by
   rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_left_comm b]
 
-protected theorem mul_two (n) : n * 2 = n + n := by rw [Nat.mul_succ, Nat.mul_one]
-
-protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mul]
-
 theorem mul_eq_zero : ∀ {m n}, n * m = 0 ↔ n = 0 ∨ m = 0
   | 0, _ => ⟨fun _ => .inr rfl, fun _ => rfl⟩
   | _, 0 => ⟨fun _ => .inl rfl, fun _ => Nat.zero_mul ..⟩

src/Init/Data/Random.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.System.IO
-import Init.Data.Int
 universe u
 
 /-!

src/Init/Omega/Int.lean

@@ -6,7 +6,6 @@ Authors: Scott Morrison
 prelude
 import Init.Data.Int.DivMod
 import Init.Data.Int.Order
-import Init.Data.Nat.Basic
 
 /-!
 # Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.

src/Init/Omega/IntList.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 prelude
 import Init.Data.List.Lemmas
 import Init.Data.Int.DivModLemmas
-import Init.Data.Int.Gcd
+import Init.Data.Nat.Gcd
 
 namespace Lean.Omega
 

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -5,8 +5,10 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.BinderPredicates
+import Init.Data.Int.Order
+import Init.Data.List.Lemmas
+import Init.Data.Nat.MinMax
 import Init.Data.Option.Lemmas
-import Init.Data.Nat.Bitwise.Lemmas
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Omega.LinearCombo
 import Init.Omega.Int
 import Init.Omega.Logic
-import Init.Data.BitVec
+import Init.Data.BitVec.Basic
 import Lean.Meta.AppBuilder
 
 /-!
@@ -176,7 +176,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
       | _, (``BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
+        r := r.insert (mkApp2 (.const ``BitVec.isLt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with