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

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 ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x

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