Lemmas about integer division

/

theorem Int.ofNat_div (m : Nat) (n : Nat) : ↑(m / n) = Int.div ↑m ↑n

theorem Int.ofNat_fdiv (m : Nat) (n : Nat) : ↑(m / n) = Int.fdiv ↑m ↑n

theorem Int.negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : Int.negSucc m / b = -(Int.div (↑m) b + 1)

@[simp]

theorem Int.zero_div (b : Int) : Int.div 0 b = 0

@[simp]

theorem Int.zero_fdiv (b : Int) : Int.fdiv 0 b = 0

@[simp]

theorem Int.div_zero (a : Int) : Int.div a 0 = 0

@[simp]

theorem Int.fdiv_zero (a : Int) : Int.fdiv a 0 = 0

theorem Int.fdiv_eq_ediv (a : Int) {b : Int} : 0 ≤ b → Int.fdiv a b = a / b

theorem Int.div_eq_ediv {a : Int} {b : Int} : 0 ≤ a → 0 ≤ b → Int.div a b = a / b

theorem Int.fdiv_eq_div {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : Int.fdiv a b = Int.div a b

@[simp]

theorem Int.div_neg (a : Int) (b : Int) : Int.div a (-b) = -Int.div a b

@[simp]

theorem Int.neg_div (a : Int) (b : Int) : Int.div (-a) b = -Int.div a b

theorem Int.neg_div_neg (a : Int) (b : Int) : Int.div (-a) (-b) = Int.div a b

theorem Int.div_nonneg {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ Int.div a b

theorem Int.fdiv_nonneg {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ Int.fdiv a b

theorem Int.ediv_nonneg {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a / b

theorem Int.div_nonpos {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : Int.div a b ≤ 0

theorem Int.fdiv_nonpos {a : Int} {b : Int} : 0 ≤ a → b ≤ 0 → Int.fdiv a b ≤ 0

theorem Int.ediv_nonpos {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0

theorem Int.fdiv_neg' {a : Int} {b : Int} : a < 0 → 0 < b → Int.fdiv a b < 0

theorem Int.ediv_neg' {a : Int} {b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0

@[simp]

theorem Int.div_one (a : Int) : Int.div a 1 = a

@[simp]

theorem Int.fdiv_one (a : Int) : Int.fdiv a 1 = a

theorem Int.div_eq_zero_of_lt {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : a < b) : Int.div a b = 0

theorem Int.ediv_eq_zero_of_lt {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a / b = 0

theorem Int.add_mul_ediv_left (a : Int) {b : Int} (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c

@[simp]

theorem Int.mul_fdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : Int.fdiv (a * b) b = a

@[simp]

theorem Int.mul_div_cancel (a : Int) {b : Int} (H : b ≠ 0) : Int.div (a * b) b = a

@[simp]

theorem Int.mul_div_cancel_left {a : Int} (b : Int) (H : a ≠ 0) : Int.div (a * b) a = b

@[simp]

theorem Int.mul_fdiv_cancel_left {a : Int} (b : Int) (H : a ≠ 0) : Int.fdiv (a * b) a = b

@[simp]

theorem Int.div_self {a : Int} (H : a ≠ 0) : Int.div a a = 1

@[simp]

theorem Int.fdiv_self {a : Int} (H : a ≠ 0) : Int.fdiv a a = 1

mod

theorem Int.ofNat_fmod (m : Nat) (n : Nat) : ↑(m % n) = Int.fmod ↑m ↑n

theorem Int.negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) : Int.negSucc m % b = b - 1 - ↑m % b

@[simp]

theorem Int.zero_mod (b : Int) : Int.mod 0 b = 0

@[simp]

theorem Int.zero_fmod (b : Int) : Int.fmod 0 b = 0

@[simp]

theorem Int.mod_zero (a : Int) : Int.mod a 0 = a

@[simp]

theorem Int.fmod_zero (a : Int) : Int.fmod a 0 = a

theorem Int.mod_add_div (a : Int) (b : Int) : Int.mod a b + b * Int.div a b = a

theorem Int.fmod_add_fdiv (a : Int) (b : Int) : Int.fmod a b + b * Int.fdiv a b = a

theorem Int.div_add_mod (a : Int) (b : Int) : b * Int.div a b + Int.mod a b = a

theorem Int.fdiv_add_fmod (a : Int) (b : Int) : b * Int.fdiv a b + Int.fmod a b = a

theorem Int.mod_def (a : Int) (b : Int) : Int.mod a b = a - b * Int.div a b

theorem Int.fmod_def (a : Int) (b : Int) : Int.fmod a b = a - b * Int.fdiv a b

theorem Int.fmod_eq_emod (a : Int) {b : Int} (hb : 0 ≤ b) : Int.fmod a b = a % b

theorem Int.mod_eq_emod {a : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : Int.mod a b = a % b

theorem Int.fmod_eq_mod {a : Int} {b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : Int.fmod a b = Int.mod a b

@[simp]

theorem Int.mod_neg (a : Int) (b : Int) : Int.mod a (-b) = Int.mod a b

@[simp]

theorem Int.emod_neg (a : Int) (b : Int) : a % -b = a % b

@[simp]

theorem Int.mod_one (a : Int) : Int.mod a 1 = 0

@[simp]

theorem Int.fmod_one (a : Int) : Int.fmod a 1 = 0

theorem Int.emod_eq_of_lt {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a

@[simp]

theorem Int.emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x

theorem Int.mod_eq_of_lt {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : a < b) : Int.mod a b = a

theorem Int.fmod_eq_of_lt {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : a < b) : Int.fmod a b = a

theorem Int.mod_nonneg {a : Int} (b : Int) : 0 ≤ a → 0 ≤ Int.mod a b

theorem Int.fmod_nonneg {a : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ Int.fmod a b

theorem Int.fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ Int.fmod a b

theorem Int.mod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : Int.mod a b < b

theorem Int.fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : Int.fmod a b < b

theorem Int.emod_two_eq (x : Int) : x % 2 = 0 ∨ x % 2 = 1

theorem Int.mod_add_div' (m : Int) (k : Int) : Int.mod m k + Int.div m k * k = m

theorem Int.div_add_mod' (m : Int) (k : Int) : Int.div m k * k + Int.mod m k = m

theorem Int.ediv_add_emod' (m : Int) (k : Int) : m / k * k + m % k = m

theorem Int.add_emod_eq_add_emod_left {m : Int} {n : Int} {k : Int} (i : Int) (H : m % n = k % n) : (i + m) % n = (i + k) % n

theorem Int.emod_add_cancel_left {m : Int} {n : Int} {k : Int} {i : Int} : (i + m) % n = (i + k) % n ↔ m % n = k % n

theorem Int.emod_sub_cancel_right {m : Int} {n : Int} {k : Int} (i : Int) : (m - i) % n = (k - i) % n ↔ m % n = k % n

theorem Int.emod_eq_emod_iff_emod_sub_eq_zero {m : Int} {n : Int} {k : Int} : m % n = k % n ↔ (m - k) % n = 0

@[simp]

theorem Int.mul_mod_left (a : Int) (b : Int) : Int.mod (a * b) b = 0

@[simp]

theorem Int.mul_fmod_left (a : Int) (b : Int) : Int.fmod (a * b) b = 0

@[simp]

theorem Int.mul_mod_right (a : Int) (b : Int) : Int.mod (a * b) a = 0

@[simp]

theorem Int.mul_fmod_right (a : Int) (b : Int) : Int.fmod (a * b) a = 0

@[simp]

theorem Int.mod_self {a : Int} : Int.mod a a = 0

@[simp]

theorem Int.fmod_self {a : Int} : Int.fmod a a = 0

theorem Int.ediv_emod_unique {a : Int} {b : Int} {r : Int} {q : Int} (h : 0 < b) : a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b

properties of / and %

@[simp]

theorem Int.mul_ediv_mul_of_pos {a : Int} (b : Int) (c : Int) (H : 0 < a) : a * b / (a * c) = b / c

@[simp]

theorem Int.mul_ediv_mul_of_pos_left (a : Int) {b : Int} (c : Int) (H : 0 < b) : a * b / (c * b) = a / c

@[simp]

theorem Int.mul_emod_mul_of_pos {a : Int} (b : Int) (c : Int) (H : 0 < a) : a * b % (a * c) = a * (b % c)

theorem Int.lt_div_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (Int.div a b + 1) * b

theorem Int.lt_ediv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a / b + 1) * b

theorem Int.lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (Int.fdiv a b + 1) * b

@[simp]

theorem Int.natAbs_div (a : Int) (b : Int) : Int.natAbs (Int.div a b) = Nat.div (Int.natAbs a) (Int.natAbs b)

theorem Int.natAbs_div_le_natAbs (a : Int) (b : Int) : Int.natAbs (a / b) ≤ Int.natAbs a

theorem Int.natAbs_div_le_natAbs.aux (a : Int) (n : Nat) : Int.natAbs (a / ↑n) ≤ Int.natAbs a

theorem Int.ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a

theorem Int.mul_div_cancel_of_mod_eq_zero {a : Int} {b : Int} (H : Int.mod a b = 0) : b * Int.div a b = a

theorem Int.div_mul_cancel_of_mod_eq_zero {a : Int} {b : Int} (H : Int.mod a b = 0) : Int.div a b * b = a

dvd

theorem Int.dvd_add_left {a : Int} {b : Int} {c : Int} (H : a ∣ c) : a ∣ b + c ↔ a ∣ b

theorem Int.dvd_add_right {a : Int} {b : Int} {c : Int} (H : a ∣ b) : a ∣ b + c ↔ a ∣ c

theorem Int.dvd_iff_dvd_of_dvd_sub {a : Int} {b : Int} {c : Int} (H : a ∣ b - c) : a ∣ b ↔ a ∣ c

theorem Int.dvd_iff_dvd_of_dvd_add {a : Int} {b : Int} {c : Int} (H : a ∣ b + c) : a ∣ b ↔ a ∣ c

theorem Int.natAbs_dvd {a : Int} {b : Int} : ↑(Int.natAbs a) ∣ b ↔ a ∣ b

theorem Int.dvd_natAbs {a : Int} {b : Int} : a ∣ ↑(Int.natAbs b) ↔ a ∣ b

theorem Int.natAbs_dvd_self {a : Int} : ↑(Int.natAbs a) ∣ a

theorem Int.dvd_natAbs_self {a : Int} : a ∣ ↑(Int.natAbs a)

theorem Int.ofNat_dvd_right {n : Nat} {z : Int} : z ∣ ↑n ↔ Int.natAbs z ∣ n

theorem Int.dvd_antisymm {a : Int} {b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b

theorem Int.dvd_of_mod_eq_zero {a : Int} {b : Int} (H : Int.mod b a = 0) : a ∣ b

theorem Int.mod_eq_zero_of_dvd {a : Int} {b : Int} : a ∣ b → Int.mod b a = 0

theorem Int.dvd_iff_mod_eq_zero (a : Int) (b : Int) : a ∣ b ↔ Int.mod b a = 0

theorem Int.dvd_sub_of_emod_eq {a : Int} {b : Int} {c : Int} (h : a % b = c) : b ∣ a - c

If a % b = c then b divides a - c.

theorem Int.div_mul_cancel {a : Int} {b : Int} (H : b ∣ a) : Int.div a b * b = a

theorem Int.mul_div_cancel' {a : Int} {b : Int} (H : a ∣ b) : a * Int.div b a = b

theorem Int.mul_div_assoc (a : Int) {b : Int} {c : Int} : c ∣ b → Int.div (a * b) c = a * Int.div b c

theorem Int.mul_div_assoc' (b : Int) {a : Int} {c : Int} (h : c ∣ a) : Int.div (a * b) c = Int.div a c * b

theorem Int.div_dvd_div {a : Int} {b : Int} {c : Int} : a ∣ b → b ∣ c → Int.div b a ∣ Int.div c a

theorem Int.eq_mul_of_div_eq_right {a : Int} {b : Int} {c : Int} (H1 : b ∣ a) (H2 : Int.div a b = c) : a = b * c

theorem Int.eq_mul_of_ediv_eq_right {a : Int} {b : Int} {c : Int} (H1 : b ∣ a) (H2 : a / b = c) : a = b * c

theorem Int.div_eq_of_eq_mul_right {a : Int} {b : Int} {c : Int} (H1 : b ≠ 0) (H2 : a = b * c) : Int.div a b = c

theorem Int.ediv_eq_of_eq_mul_right {a : Int} {b : Int} {c : Int} (H1 : b ≠ 0) (H2 : a = b * c) : a / b = c

theorem Int.eq_div_of_mul_eq_right {a : Int} {b : Int} {c : Int} (H1 : a ≠ 0) (H2 : a * b = c) : b = Int.div c a

theorem Int.eq_ediv_of_mul_eq_right {a : Int} {b : Int} {c : Int} (H1 : a ≠ 0) (H2 : a * b = c) : b = c / a

theorem Int.div_eq_iff_eq_mul_right {a : Int} {b : Int} {c : Int} (H : b ≠ 0) (H' : b ∣ a) : Int.div a b = c ↔ a = b * c

theorem Int.ediv_eq_iff_eq_mul_right {a : Int} {b : Int} {c : Int} (H : b ≠ 0) (H' : b ∣ a) : a / b = c ↔ a = b * c

theorem Int.div_eq_iff_eq_mul_left {a : Int} {b : Int} {c : Int} (H : b ≠ 0) (H' : b ∣ a) : Int.div a b = c ↔ a = c * b

theorem Int.ediv_eq_iff_eq_mul_left {a : Int} {b : Int} {c : Int} (H : b ≠ 0) (H' : b ∣ a) : a / b = c ↔ a = c * b

theorem Int.eq_mul_of_div_eq_left {a : Int} {b : Int} {c : Int} (H1 : b ∣ a) (H2 : Int.div a b = c) : a = c * b

theorem Int.eq_mul_of_ediv_eq_left {a : Int} {b : Int} {c : Int} (H1 : b ∣ a) (H2 : a / b = c) : a = c * b

theorem Int.div_eq_of_eq_mul_left {a : Int} {b : Int} {c : Int} (H1 : b ≠ 0) (H2 : a = c * b) : Int.div a b = c

theorem Int.ediv_eq_of_eq_mul_left {a : Int} {b : Int} {c : Int} (H1 : b ≠ 0) (H2 : a = c * b) : a / b = c

theorem Int.eq_zero_of_div_eq_zero {d : Int} {n : Int} (h : d ∣ n) (H : Int.div n d = 0) : n = 0

theorem Int.eq_zero_of_ediv_eq_zero {d : Int} {n : Int} (h : d ∣ n) (H : n / d = 0) : n = 0

theorem Int.div_eq_ediv_of_dvd {a : Int} {b : Int} (h : b ∣ a) : Int.div a b = a / b

theorem Int.fdiv_eq_ediv_of_dvd {a : Int} {b : Int} : b ∣ a → Int.fdiv a b = a / b

theorem Int.sub_ediv_of_dvd_sub {a : Int} {b : Int} {c : Int} (hcab : c ∣ a - b) : (a - b) / c = a / c - b / c

@[simp]

theorem Int.div_left_inj {a : Int} {b : Int} {d : Int} (hda : d ∣ a) (hdb : d ∣ b) : Int.div a d = Int.div b d ↔ a = b

@[simp]

theorem Int.ediv_left_inj {a : Int} {b : Int} {d : Int} (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

theorem Int.div_sign (a : Int) (b : Int) : Int.div a (Int.sign b) = a * Int.sign b

theorem Int.ediv_sign (a : Int) (b : Int) : a / Int.sign b = a * Int.sign b

theorem Int.sign_eq_div_abs (a : Int) : Int.sign a = Int.div a ↑(Int.natAbs a)

theorem Int.mul_sign (i : Int) : i * Int.sign i = ↑(Int.natAbs i)

theorem Int.le_of_dvd {a : Int} {b : Int} (bpos : 0 < b) (H : a ∣ b) : a ≤ b

theorem Int.eq_one_of_dvd_one {a : Int} (H : 0 ≤ a) (H' : a ∣ 1) : a = 1

theorem Int.eq_one_of_mul_eq_one_right {a : Int} {b : Int} (H : 0 ≤ a) (H' : a * b = 1) : a = 1

theorem Int.eq_one_of_mul_eq_one_left {a : Int} {b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1

theorem Int.le_of_mul_le_mul_left {a : Int} {b : Int} {c : Int} (w : a * b ≤ a * c) (h : 0 < a) : b ≤ c

theorem Int.le_of_mul_le_mul_right {a : Int} {b : Int} {c : Int} (w : b * a ≤ c * a) (h : 0 < a) : b ≤ c

theorem Int.lt_of_mul_lt_mul_left {a : Int} {b : Int} {c : Int} (w : a * b < a * c) (h : 0 ≤ a) : b < c

theorem Int.lt_of_mul_lt_mul_right {a : Int} {b : Int} {c : Int} (w : b * a < c * a) (h : 0 ≤ a) : b < c

bmod ("balanced" mod)

theorem Int.emod_bmod {x : Int} {m : Nat} : Int.bmod (x % ↑m) m = Int.bmod x m

@[simp]

theorem Int.bmod_bmod {x : Int} {m : Nat} : Int.bmod (Int.bmod x m) m = Int.bmod x m

@[simp]

theorem Int.bmod_zero {m : Nat} : Int.bmod 0 m = 0

theorem Int.dvd_bmod_sub_self {x : Int} {m : Nat} : ↑m ∣ Int.bmod x m - x

theorem Int.le_bmod {x : Int} {m : Nat} (h : 0 < m) : -(↑m / 2) ≤ Int.bmod x m

theorem Int.bmod_lt {x : Int} {m : Nat} (h : 0 < m) : Int.bmod x m < (↑m + 1) / 2

theorem Int.bmod_le {x : Int} {m : Nat} (h : 0 < m) : Int.bmod x m ≤ (↑m - 1) / 2

theorem Int.bmod_natAbs_plus_one (x : Int) (w : 1 < Int.natAbs x) : Int.bmod x (Int.natAbs x + 1) = -Int.sign x

/ and ordering

theorem Int.ediv_mul_le (a : Int) {b : Int} (H : b ≠ 0) : a / b * b ≤ a

theorem Int.ediv_le_of_le_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a ≤ b * c) : a / c ≤ b

theorem Int.mul_lt_of_lt_ediv {a : Int} {b : Int} {c : Int} (H : 0 < c) (H3 : a < b / c) : a * c < b

theorem Int.mul_le_of_le_ediv {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a ≤ b / c) : a * c ≤ b

theorem Int.le_ediv_of_mul_le {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a * c ≤ b) : a ≤ b / c

theorem Int.le_ediv_iff_mul_le {a : Int} {b : Int} {c : Int} (H : 0 < c) : a ≤ b / c ↔ a * c ≤ b

theorem Int.ediv_le_ediv {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a ≤ b) : a / c ≤ b / c

theorem Int.ediv_lt_of_lt_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a < b * c) : a / c < b

theorem Int.lt_mul_of_ediv_lt {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a / c < b) : a < b * c

theorem Int.ediv_lt_iff_lt_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) : a / c < b ↔ a < b * c

theorem Int.le_mul_of_ediv_le {a : Int} {b : Int} {c : Int} (H1 : 0 ≤ b) (H2 : b ∣ a) (H3 : a / b ≤ c) : a ≤ c * b

theorem Int.lt_ediv_of_mul_lt {a : Int} {b : Int} {c : Int} (H1 : 0 ≤ b) (H2 : b ∣ c) (H3 : a * b < c) : a < c / b

theorem Int.lt_ediv_iff_mul_lt {a : Int} {b : Int} (c : Int) (H : 0 < c) (H' : c ∣ b) : a < b / c ↔ a * c < b

theorem Int.ediv_pos_of_pos_of_dvd {a : Int} {b : Int} (H1 : 0 < a) (H2 : 0 ≤ b) (H3 : b ∣ a) : 0 < a / b

theorem Int.ediv_eq_ediv_of_mul_eq_mul {a : Int} {b : Int} {c : Int} {d : Int} (H2 : d ∣ c) (H3 : b ≠ 0) (H4 : d ≠ 0) (H5 : a * d = b * c) : a / b = c / d

The following lemmas have been commented out here for a while, and need restoration.