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