Further lemmas about Nat.div and Nat.mod, with the convenience of having omega available.

theorem Nat.mod_add_mod_lt (a b : Nat) {c : Nat} (h : 0 < c) : a % c + b % c < 2 * c - 1

theorem Nat.mod_add_mod_eq {a b c : Nat} : a % c + b % c = (a + b) % c + if a % c + b % c < c then 0 else c

theorem Nat.add_mod_eq_sub {a b c : Nat} : (a + b) % c = a % c + b % c - if a % c + b % c < c then 0 else c

theorem Nat.lt_div_iff_mul_lt {k x y : Nat} (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1)

theorem Nat.div_le_iff_le_mul {k x y : Nat} (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1

theorem Nat.div_eq_iff {k x y : Nat} (h : 0 < k) : x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1

theorem Nat.lt_of_div_eq_zero {k x : Nat} (h : 0 < k) (h' : x / k = 0) : x < k

theorem Nat.div_eq_zero_iff_lt {k x : Nat} (h : 0 < k) : x / k = 0 ↔ x < k

theorem Nat.div_mul_self_eq_mod_sub_self {x k : Nat} : x / k * k = x - x % k

theorem Nat.mul_div_self_eq_mod_sub_self {x k : Nat} : k * (x / k) = x - x % k

theorem Nat.lt_div_mul_self {k x : Nat} (h : 0 < k) (w : k ≤ x) : x - k < x / k * k

theorem Nat.div_pos {b a : Nat} (hba : b ≤ a) (hb : 0 < b) : 0 < a / b

theorem Nat.div_le_div_left {c b a : Nat} (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c

theorem Nat.div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) : x / (y + z) ≤ x / z

theorem Nat.succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) : (a + 1) / b = a / b + 1

theorem Nat.succ_div_of_mod_eq_zero {a b : Nat} (h : (a + 1) % b = 0) : (a + 1) / b = a / b + 1

theorem Nat.succ_div_of_not_dvd {a b : Nat} (h : ¬b ∣ a + 1) : (a + 1) / b = a / b

theorem Nat.succ_div_of_mod_ne_zero {a b : Nat} (h : (a + 1) % b ≠ 0) : (a + 1) / b = a / b

theorem Nat.succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0

theorem Nat.add_div {a b c : Nat} (h : 0 < c) : (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0

theorem Nat.mod_add_mod_lt_of_add_mod_eq_sub_one {c a b : Nat} (w : 0 < c) (h : (a + b) % c = c - 1) : a % c + b % c < c

If (a + b) % c = c - 1, then a % c + b % c < c, because a % c + b % c can not reach 2*c - 1.

theorem Nat.add_div_of_dvd_add_add_one {c a b : Nat} (h : c ∣ a + b + 1) : (a + b) / c = a / c + b / c

theorem Nat.div_lt_of_lt {a b c : Nat} (ha : a < c) : a / b < c

theorem Nat.div_mod_eq_div {a b c : Nat} (ha : a < c) : a / b % c = a / b

theorem Nat.div_mod_eq_mod_div_mod {a b c : Nat} (ha : a < c) (hb : b < c) : a / b % c = a % c / (b % c)

theorem Nat.mod_mod_eq_mod_of_lt_right {a b c : Nat} (ha : a < c) : a % b % c = a % b

theorem Nat.mod_mod_eq_mod_mod_mod {a b c : Nat} (ha : a < c) (hb : b < c) : a % b % c = a % c % (b % c)

theorem Nat.mod_mod_eq_mod_mod_of_dvd {a b c : Nat} (h : b ∣ c) : a % b % c = a % c % b

theorem Nat.mod_mod_of_dvd' {a b c : Nat} (h : b ∣ c) : a % b % c = a % b

theorem Nat.mod_mod_eq_mod_mod_mod_of_dvd {a b c : Nat} (hb : b ∣ c) : a % b % c = a % c % (b % c)