Lemmas about integer division needed to bootstrap omega.

/

@[simp]

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

@[simp]

theorem Int.zero_ediv (b : Int) : 0 / b = 0

@[simp]

theorem Int.ediv_zero (a : Int) : a / 0 = 0

@[simp]

theorem Int.ediv_neg (a : Int) (b : Int) : a / -b = -(a / b)

theorem Int.div_def (a : Int) (b : Int) : a / b = Int.ediv a b

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

theorem Int.add_ediv_of_dvd_right {a : Int} {b : Int} {c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c

theorem Int.add_ediv_of_dvd_left {a : Int} {b : Int} {c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c

@[simp]

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

@[simp]

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

theorem Int.div_nonneg_iff_of_pos {a : Int} {b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0

mod

theorem Int.mod_def' (m : Int) (n : Int) : m % n = Int.emod m n

theorem Int.ofNat_mod (m : Nat) (n : Nat) : ↑(m % n) = Int.mod ↑m ↑n

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

@[simp]

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

@[simp]

theorem Int.zero_emod (b : Int) : 0 % b = 0

@[simp]

theorem Int.emod_zero (a : Int) : a % 0 = a

theorem Int.emod_add_ediv (a : Int) (b : Int) : a % b + b * (a / b) = a

theorem Int.emod_add_ediv.aux (m : Nat) (n : Nat) : ↑n - (↑m % ↑n + 1) - (↑n * (↑m / ↑n) + ↑n) = Int.negSucc m

theorem Int.ediv_add_emod (a : Int) (b : Int) : b * (a / b) + a % b = a

theorem Int.emod_def (a : Int) (b : Int) : a % b = a - b * (a / b)

theorem Int.emod_nonneg (a : Int) {b : Int} : b ≠ 0 → 0 ≤ a % b

theorem Int.emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b

theorem Int.mul_ediv_self_le {x : Int} {k : Int} (h : k ≠ 0) : k * (x / k) ≤ x

theorem Int.lt_mul_ediv_self_add {x : Int} {k : Int} (h : 0 < k) : x < k * (x / k) + k

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

@[simp]

theorem Int.add_mul_emod_self {a : Int} {b : Int} {c : Int} : (a + b * c) % c = a % c

@[simp]

theorem Int.add_mul_emod_self_left (a : Int) (b : Int) (c : Int) : (a + b * c) % b = a % b

@[simp]

theorem Int.add_emod_self {a : Int} {b : Int} : (a + b) % b = a % b

@[simp]

theorem Int.add_emod_self_left {a : Int} {b : Int} : (a + b) % a = b % a

theorem Int.neg_emod {a : Int} {b : Int} : -a % b = (b - a) % b

@[simp]

theorem Int.emod_add_emod (m : Int) (n : Int) (k : Int) : (m % n + k) % n = (m + k) % n

@[simp]

theorem Int.add_emod_emod (m : Int) (n : Int) (k : Int) : (m + n % k) % k = (m + n) % k

theorem Int.add_emod (a : Int) (b : Int) (n : Int) : (a + b) % n = (a % n + b % n) % n

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

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

@[simp]

theorem Int.mul_emod_left (a : Int) (b : Int) : a * b % b = 0

@[simp]

theorem Int.mul_emod_right (a : Int) (b : Int) : a * b % a = 0

theorem Int.mul_emod (a : Int) (b : Int) (n : Int) : a * b % n = a % n * (b % n) % n

theorem Int.emod_self {a : Int} : a % a = 0

@[simp]

theorem Int.emod_emod_of_dvd (n : Int) {m : Int} {k : Int} (h : m ∣ k) : n % k % m = n % m

@[simp]

theorem Int.emod_emod (a : Int) (b : Int) : a % b % b = a % b

theorem Int.sub_emod (a : Int) (b : Int) (n : Int) : (a - b) % n = (a % n - b % n) % n

properties of / and %

theorem Int.mul_ediv_cancel_of_emod_eq_zero {a : Int} {b : Int} (H : a % b = 0) : b * (a / b) = a

theorem Int.ediv_mul_cancel_of_emod_eq_zero {a : Int} {b : Int} (H : a % b = 0) : a / b * b = a

dvd

theorem Int.dvd_zero (n : Int) : n ∣ 0

theorem Int.dvd_refl (n : Int) : n ∣ n

theorem Int.one_dvd (n : Int) : 1 ∣ n

theorem Int.dvd_trans {a : Int} {b : Int} {c : Int} : a ∣ b → b ∣ c → a ∣ c

@[simp]

theorem Int.zero_dvd {n : Int} : 0 ∣ n ↔ n = 0

theorem Int.neg_dvd {a : Int} {b : Int} : -a ∣ b ↔ a ∣ b

theorem Int.dvd_neg {a : Int} {b : Int} : a ∣ -b ↔ a ∣ b

theorem Int.dvd_mul_right (a : Int) (b : Int) : a ∣ a * b

theorem Int.dvd_mul_left (a : Int) (b : Int) : b ∣ a * b

theorem Int.dvd_add {a : Int} {b : Int} {c : Int} : a ∣ b → a ∣ c → a ∣ b + c

theorem Int.dvd_sub {a : Int} {b : Int} {c : Int} : a ∣ b → a ∣ c → a ∣ b - c

theorem Int.ofNat_dvd {m : Nat} {n : Nat} : ↑m ∣ ↑n ↔ m ∣ n

@[simp]

theorem Int.natAbs_dvd_natAbs {a : Int} {b : Int} : Int.natAbs a ∣ Int.natAbs b ↔ a ∣ b

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

theorem Int.dvd_of_emod_eq_zero {a : Int} {b : Int} (H : b % a = 0) : a ∣ b

theorem Int.dvd_emod_sub_self {x : Int} {m : Nat} : ↑m ∣ x % ↑m - x

theorem Int.emod_eq_zero_of_dvd {a : Int} {b : Int} : a ∣ b → b % a = 0

theorem Int.dvd_iff_emod_eq_zero (a : Int) (b : Int) : a ∣ b ↔ b % a = 0

theorem Int.emod_pos_of_not_dvd {a : Int} {b : Int} (h : ¬a ∣ b) : a = 0 ∨ 0 < b % a

instance Int.decidableDvd : DecidableRel fun (x x_1 : Int) => x ∣ x_1

Equations

• Int.decidableDvd x✝ x = decidable_of_decidable_of_iff ⋯

theorem Int.ediv_mul_cancel {a : Int} {b : Int} (H : b ∣ a) : a / b * b = a

theorem Int.mul_ediv_cancel' {a : Int} {b : Int} (H : a ∣ b) : a * (b / a) = b

theorem Int.mul_ediv_assoc (a : Int) {b : Int} {c : Int} : c ∣ b → a * b / c = a * (b / c)

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

theorem Int.neg_ediv_of_dvd {a : Int} {b : Int} : b ∣ a → -a / b = -(a / b)

theorem Int.sub_ediv_of_dvd (a : Int) {b : Int} {c : Int} (hcb : c ∣ b) : (a - b) / c = a / c - b / c

@[simp]

theorem Int.ediv_one (a : Int) : a / 1 = a

@[simp]

theorem Int.emod_one (a : Int) : a % 1 = 0

@[simp]

theorem Int.ediv_self {a : Int} (H : a ≠ 0) : a / a = 1

@[simp]

theorem Int.Int.emod_sub_cancel (x : Int) (y : Int) : (x - y) % y = x % y

bmod

@[simp]

theorem Int.bmod_emod {x : Int} {m : Nat} : Int.bmod x m % ↑m = x % ↑m

@[simp]

theorem Int.emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % ↑n) n = Int.bmod x n

theorem Int.bmod_def (x : Int) (m : Nat) : Int.bmod x m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m

theorem Int.bmod_pos (x : Int) (m : Nat) (p : x % ↑m < (↑m + 1) / 2) : Int.bmod x m = x % ↑m

theorem Int.bmod_neg (x : Int) (m : Nat) (p : x % ↑m ≥ (↑m + 1) / 2) : Int.bmod x m = x % ↑m - ↑m

@[simp]

theorem Int.bmod_one_is_zero (x : Int) : Int.bmod x 1 = 0

@[simp]

theorem Int.bmod_add_cancel (x : Int) (n : Nat) : Int.bmod (x + ↑n) n = Int.bmod x n

@[simp]

theorem Int.bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + ↑n * k) n = Int.bmod x n

@[simp]

theorem Int.bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - ↑n) n = Int.bmod x n

@[simp]

theorem Int.emod_add_bmod_congr {y : Int} (x : Int) (n : Nat) : Int.bmod (x % ↑n + y) n = Int.bmod (x + y) n

@[simp]

theorem Int.bmod_add_bmod_congr {x : Int} {n : Nat} {y : Int} : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n

@[simp]

theorem Int.add_bmod_bmod {x : Int} {y : Int} {n : Nat} : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n