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

source
theorem Nat.mod_add_mod_lt (a b : Nat) {c : Nat} (h : 0 < c) :
a % c + b % c < 2 * c - 1
source
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
source
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
source
theorem Nat.lt_div_iff_mul_lt {k x y : Nat} (h : 0 < k) :
x < y / k ↔ x * k < y - (k - 1)
source
theorem Nat.div_le_iff_le_mul {k x y : Nat} (h : 0 < k) :
x / k ≤ y ↔ x ≤ y * k + k - 1
source
theorem Nat.div_eq_iff {k x y : Nat} (h : 0 < k) :
x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1
source
theorem Nat.lt_of_div_eq_zero {k x : Nat} (h : 0 < k) (h' : x / k = 0) :
x < k
source
theorem Nat.div_eq_zero_iff_lt {k x : Nat} (h : 0 < k) :
x / k = 0 ↔ x < k
source
theorem Nat.div_mul_self_eq_mod_sub_self {x k : Nat} :
x / k * k = x - x % k
source
theorem Nat.mul_div_self_eq_mod_sub_self {x k : Nat} :
k * (x / k) = x - x % k
source
theorem Nat.lt_div_mul_self {k x : Nat} (h : 0 < k) (w : k ≤ x) :
x - k < x / k * k
source
theorem Nat.div_pos {b a : Nat} (hba : b ≤ a) (hb : 0 < b) :
0 < a / b
source
theorem Nat.div_le_div_left {c b a : Nat} (hcb : c ≤ b) (hc : 0 < c) :
a / b ≤ a / c
source
theorem Nat.div_le_div {a b c d : Nat} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) :
a / c ≤ b / d
source
theorem Nat.div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
x / (y + z) ≤ x / z
source
theorem Nat.succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) :
(a + 1) / b = a / b + 1
source
theorem Nat.succ_div_of_mod_eq_zero {a b : Nat} (h : (a + 1) % b = 0) :
(a + 1) / b = a / b + 1
source
theorem Nat.succ_div_of_not_dvd {a b : Nat} (h : ¬b ∣ a + 1) :
(a + 1) / b = a / b
source
theorem Nat.succ_div_of_mod_ne_zero {a b : Nat} (h : (a + 1) % b ≠ 0) :
(a + 1) / b = a / b
source
theorem Nat.succ_div {a b : Nat} :
(a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
source
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
source
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`.

source
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
source
theorem Nat.div_lt_of_lt {a b c : Nat} (ha : a < c) :
a / b < c
source
theorem Nat.div_mod_eq_div {a b c : Nat} (ha : a < c) :
a / b % c = a / b
source
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)
source
theorem Nat.mod_mod_eq_mod_of_lt_right {a b c : Nat} (ha : a < c) :
a % b % c = a % b
source
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)
source
theorem Nat.mod_mod_eq_mod_mod_of_dvd {a b c : Nat} (h : b ∣ c) :
a % b % c = a % c % b
source
theorem Nat.mod_mod_of_dvd' {a b c : Nat} (h : b ∣ c) :
a % b % c = a % b
source
theorem Nat.mod_mod_eq_mod_mod_mod_of_dvd {a b c : Nat} (hb : b ∣ c) :
a % b % c = a % c % (b % c)
source
theorem Nat.mod_eq_mod_iff {x y z : Nat} :
x % z = y % z ↔ ∃ (k₁ : Nat), ∃ (k₂ : Nat), x + k₁ * z = y + k₂ * z