Further lemmas about integer division, now that omega is available.

dvd

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Int.negSucc_dvd {a : Nat} {b : Int} : negSucc a ∣ b ↔ ↑(a + 1) ∣ b

@[simp]

theorem Int.dvd_negSucc {a : Int} {b : Nat} : a ∣ negSucc b ↔ a ∣ ↑(b + 1)

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 b : Int} (H : 0 ≤ a) (H' : a * b = 1) : a = 1

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

instance Int.decidableDvd : DecidableRel fun (x1 x2 : Int) => x1 ∣ x2

Equations

• x✝¹.decidableDvd x✝ = decidable_of_decidable_of_iff ⋯

theorem Int.mul_dvd_mul_iff_left {a b c : Int} (h : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c

theorem Int.mul_dvd_mul_iff_right {a b c : Int} (h : a ≠ 0) : b * a ∣ c * a ↔ b ∣ c

*div zero

@[simp]

theorem Int.zero_tdiv (b : Int) : tdiv 0 b = 0

@[simp]

theorem Int.tdiv_zero (a : Int) : a.tdiv 0 = 0

@[simp]

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

@[simp]

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

preliminaries for div equivalences

theorem Int.negSucc_emod_ofNat_succ_eq_zero_iff {a b : Nat} : negSucc a % (↑b + 1) = 0 ↔ (a + 1) % (b + 1) = 0

theorem Int.negSucc_emod_negSucc_eq_zero_iff {a b : Nat} : negSucc a % negSucc b = 0 ↔ (a + 1) % (b + 1) = 0

div equivalences

theorem Int.tdiv_eq_ediv_of_nonneg {a b : Int} : 0 ≤ a → a.tdiv b = a / b

theorem Int.tdiv_eq_ediv {a b : Int} : a.tdiv b = a / b + if 0 ≤ a ∨ b ∣ a then 0 else b.sign

theorem Int.ediv_eq_tdiv {a b : Int} : a / b = a.tdiv b - if 0 ≤ a ∨ b ∣ a then 0 else b.sign

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

theorem Int.fdiv_eq_ediv {a b : Int} : a.fdiv b = a / b - if 0 ≤ b ∨ b ∣ a then 0 else 1

theorem Int.ediv_eq_fdiv {a b : Int} : a / b = a.fdiv b + if 0 ≤ b ∨ b ∣ a then 0 else 1

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

theorem Int.fdiv_eq_tdiv {a b : Int} : a.fdiv b = a.tdiv b - if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else 1 else if 0 ≤ b then b.sign else 1 + b.sign

theorem Int.tdiv_eq_fdiv {a b : Int} : a.tdiv b = a.fdiv b + if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else 1 else if 0 ≤ b then b.sign else 1 + b.sign

theorem Int.tdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.tdiv b = a / b

theorem Int.fdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.fdiv b = a / b

mod zero

@[simp]

theorem Int.zero_tmod (b : Int) : tmod 0 b = 0

@[simp]

theorem Int.tmod_zero (a : Int) : a.tmod 0 = a

@[simp]

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

@[simp]

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

mod definitions

theorem Int.tmod_add_tdiv (a b : Int) : a.tmod b + b * a.tdiv b = a

theorem Int.tdiv_add_tmod (a b : Int) : b * a.tdiv b + a.tmod b = a

theorem Int.tmod_add_tdiv' (m k : Int) : m.tmod k + m.tdiv k * k = m

Variant of tmod_add_tdiv with the multiplication written the other way around.

theorem Int.tdiv_add_tmod' (m k : Int) : m.tdiv k * k + m.tmod k = m

Variant of tdiv_add_tmod with the multiplication written the other way around.

theorem Int.tmod_def (a b : Int) : a.tmod b = a - b * a.tdiv b

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

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

Variant of fmod_add_fdiv with the multiplication written the other way around.

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

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

Variant of fdiv_add_fmod with the multiplication written the other way around.

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

mod equivalences

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

theorem Int.fmod_eq_emod {a b : Int} : a.fmod b = a % b + if 0 ≤ b ∨ b ∣ a then 0 else b

theorem Int.emod_eq_fmod {a b : Int} : a % b = a.fmod b - if 0 ≤ b ∨ b ∣ a then 0 else b

theorem Int.tmod_eq_emod_of_nonneg {a b : Int} (ha : 0 ≤ a) : a.tmod b = a % b

theorem Int.tmod_eq_emod {a b : Int} : a.tmod b = a % b - ↑(if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs)

theorem Int.emod_eq_tmod {a b : Int} : a % b = a.tmod b + ↑(if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs)

theorem Int.fmod_eq_tmod_of_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : a.fmod b = a.tmod b

theorem Int.fmod_eq_tmod {a b : Int} : a.fmod b = a.tmod b + if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else b else if 0 ≤ b then ↑b.natAbs else 2 * ↑b.toNat

theorem Int.tmod_eq_fmod {a b : Int} : a.tmod b = a.fmod b - if b ∣ a then 0 else if 0 ≤ a then if 0 ≤ b then 0 else b else if 0 ≤ b then ↑b.natAbs else 2 * ↑b.toNat

/ ediv

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

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

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

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

theorem Int.ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b

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

theorem Int.ediv_eq_zero_of_lt {a 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_ediv_mul_of_pos {a : Int} (b 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

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

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

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

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

emod

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

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

theorem Int.emod_negSucc (m : Nat) (n : Int) : negSucc m % n = subNatNat n.natAbs (m % n.natAbs).succ

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Int.neg_emod_self (a : Int) : -a % a = 0

@[simp]

theorem Int.emod_sub_emod (m n k : Int) : (m % n - k) % n = (m - k) % n

@[simp]

theorem Int.sub_emod_emod (m n k : Int) : (m - n % k) % k = (m - n) % k

theorem Int.emod_eq_of_lt {a 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

properties of / and %

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

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

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

theorem Int.emod_sub_cancel_right {m n 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 n k : Int} : m % n = k % n ↔ (m - k) % n = 0

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int.neg_mul_ediv_cancel (a b : Int) (h : b ≠ 0) : -(a * b) / b = -a

@[simp]

theorem Int.neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b

@[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.neg_ediv_self (a : Int) (h : a ≠ 0) : -a / a = -1

@[simp]

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

@[simp]

theorem Int.add_neg_emod_self (a b : Int) : (a + -b) % b = a % b

@[simp]

theorem Int.neg_add_emod_self (a b : Int) : (-a + b) % a = b % a

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

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

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

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

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

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

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

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

@[simp]

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

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

/ and ordering

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

tdiv

@[simp]

theorem Int.tdiv_neg (a b : Int) : a.tdiv (-b) = -a.tdiv b

We don't give tdiv versions of

• add_mul_ediv_right : c ≠ 0 → (a + b * c) / c = a / c + b
• add_mul_ediv_left : b ≠ 0 → (a + b * c) / b = a / b + c
• add_ediv_of_dvd_right : c ∣ b → (a + b) / c = a / c + b / c
• add_ediv_of_dvd_left : c ∣ a → (a + b) / c = a / c + b / c because they all involve awkward off-by-one corrections.

@[simp]

theorem Int.mul_tdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b).tdiv b = a

@[simp]

theorem Int.mul_tdiv_cancel_left {a : Int} (b : Int) (H : a ≠ 0) : (a * b).tdiv a = b

theorem Int.tdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.tdiv b

theorem Int.tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a.tdiv b

theorem Int.tdiv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a.tdiv b ≤ 0

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int.tdiv_one (a : Int) : a.tdiv 1 = a

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

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

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

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

@[simp]

theorem Int.neg_tdiv (a b : Int) : (-a).tdiv b = -a.tdiv b

theorem Int.neg_tdiv_neg (a b : Int) : (-a).tdiv (-b) = a.tdiv b

@[simp]

theorem Int.tdiv_self {a : Int} (H : a ≠ 0) : a.tdiv a = 1

theorem Int.mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * a.tdiv b = a

theorem Int.tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a

theorem Int.dvd_of_tmod_eq_zero {a b : Int} (H : b.tmod a = 0) : a ∣ b

theorem Int.mul_tdiv_assoc (a : Int) {b c : Int} : c ∣ b → (a * b).tdiv c = a * b.tdiv c

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

theorem Int.tdiv_dvd_tdiv {a b c : Int} : a ∣ b → b ∣ c → b.tdiv a ∣ c.tdiv a

@[simp]

theorem Int.natAbs_tdiv (a b : Int) : (a.tdiv b).natAbs = a.natAbs.div b.natAbs

tmod

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

@[simp]

theorem Int.tmod_one (a : Int) : a.tmod 1 = 0

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

theorem Int.tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.tmod b < b

theorem Int.tmod_nonneg {a : Int} (b : Int) : 0 ≤ a → 0 ≤ a.tmod b

@[simp]

theorem Int.tmod_neg (a b : Int) : a.tmod (-b) = a.tmod b

@[simp]

theorem Int.mul_tmod_left (a b : Int) : (a * b).tmod b = 0

@[simp]

theorem Int.mul_tmod_right (a b : Int) : (a * b).tmod a = 0

theorem Int.tmod_eq_zero_of_dvd {a b : Int} : a ∣ b → b.tmod a = 0

theorem Int.dvd_iff_tmod_eq_zero {a b : Int} : a ∣ b ↔ b.tmod a = 0

@[simp]

theorem Int.neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0

@[simp]

theorem Int.neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0

theorem Int.tdiv_mul_cancel {a b : Int} (H : b ∣ a) : a.tdiv b * b = a

theorem Int.mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b

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

@[simp]

theorem Int.tmod_self {a : Int} : a.tmod a = 0

@[simp]

theorem Int.neg_tmod_self (a : Int) : (-a).tmod a = 0

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

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

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

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

theorem Int.eq_zero_of_tdiv_eq_zero {d n : Int} (h : d ∣ n) (H : n.tdiv d = 0) : n = 0

@[simp]

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

theorem Int.tdiv_sign (a b : Int) : a.tdiv b.sign = a * b.sign

theorem Int.sign_eq_tdiv_abs (a : Int) : a.sign = a.tdiv ↑a.natAbs

fdiv

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

fmod

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

bmod

@[simp]

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

theorem Int.bdiv_add_bmod (x : Int) (m : Nat) : ↑m * x.bdiv m + x.bmod m = x

theorem Int.bmod_add_bdiv (x : Int) (m : Nat) : x.bmod m + ↑m * x.bdiv m = x

theorem Int.bdiv_add_bmod' (x : Int) (m : Nat) : x.bdiv m * ↑m + x.bmod m = x

theorem Int.bmod_add_bdiv' (x : Int) (m : Nat) : x.bmod m + x.bdiv m * ↑m = x

theorem Int.bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) : x.bmod m = x - ↑m * x.bdiv m

theorem Int.bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) : x.bmod m = x - x.bdiv m * ↑m

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int.bmod_sub_bmod_congr {x : Int} {n : Nat} {y : Int} : (x.bmod n - y).bmod n = (x - y).bmod n

theorem Int.add_bmod_eq_add_bmod_right {x : Int} {n : Nat} {y : Int} (i : Int) (H : x.bmod n = y.bmod n) : (x + i).bmod n = (y + i).bmod n

theorem Int.bmod_add_cancel_right {x : Int} {n : Nat} {y : Int} (i : Int) : (x + i).bmod n = (y + i).bmod n ↔ x.bmod n = y.bmod n

@[simp]

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

@[simp]

theorem Int.sub_bmod_bmod {x y : Int} {n : Nat} : (x - y.bmod n).bmod n = (x - y).bmod n

@[simp]

theorem Int.bmod_mul_bmod {x : Int} {n : Nat} {y : Int} : (x.bmod n * y).bmod n = (x * y).bmod n

@[simp]

theorem Int.mul_bmod_bmod {x y : Int} {n : Nat} : (x * y.bmod n).bmod n = (x * y).bmod n

theorem Int.add_bmod (a b : Int) (n : Nat) : (a + b).bmod n = (a.bmod n + b.bmod n).bmod n

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem Int.bmod_neg_bmod {x : Int} {n : Nat} : (-x.bmod n).bmod n = (-x).bmod n

Helper theorems for dvd simproc

theorem Int.dvd_eq_true_of_mod_eq_zero {a b : Int} (h : (b % a == 0) = true) : (a ∣ b) = True

theorem Int.dvd_eq_false_of_mod_ne_zero {a b : Int} (h : (b % a != 0) = true) : (a ∣ b) = False