theorem Nat.div_rec_lemma {x : Nat} {y : Nat} : 0 < y ∧ y ≤ x → x - y < x

@[extern lean_nat_div]

def Nat.div (x : Nat) (y : Nat) : Nat

Equations

• Nat.div x y = if 0 < y ∧ y ≤ x then Nat.div (x - y) y + 1 else 0

instance Nat.instDivNat : Div Nat

Equations

• Nat.instDivNat = { div := Nat.div }

theorem Nat.div_eq (x : Nat) (y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0

theorem Nat.div.inductionOn {motive : Nat → Nat → Sort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) (base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y) : motive x y

theorem Nat.div_le_self (n : Nat) (k : Nat) : n / k ≤ n

theorem Nat.div_lt_self {n : Nat} {k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n

@[extern lean_nat_mod]

def Nat.modCore (x : Nat) (y : Nat) : Nat

Equations

• Nat.modCore x y = if 0 < y ∧ y ≤ x then Nat.modCore (x - y) y else x

@[extern lean_nat_mod]

def Nat.mod : Nat → Nat → Nat

Equations

• Nat.mod x✝ x = match x✝, x with | 0, x => 0 | x@h:(Nat.succ n), y => Nat.modCore x y

instance Nat.instModNat : Mod Nat

Equations

• Nat.instModNat = { mod := Nat.mod }

theorem Nat.modCore_eq_mod (x : Nat) (y : Nat) : Nat.modCore x y = x % y

theorem Nat.mod_eq (x : Nat) (y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x

theorem Nat.mod.inductionOn {motive : Nat → Nat → Sort u} (x : Nat) (y : Nat) (ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y) (base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y) : motive x y

@[simp]

theorem Nat.mod_zero (a : Nat) : a % 0 = a

theorem Nat.mod_eq_of_lt {a : Nat} {b : Nat} (h : a < b) : a % b = a

theorem Nat.mod_eq_sub_mod {a : Nat} {b : Nat} (h : a ≥ b) : a % b = (a - b) % b

theorem Nat.mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y

theorem Nat.mod_le (x : Nat) (y : Nat) : x % y ≤ x

@[simp]

theorem Nat.zero_mod (b : Nat) : 0 % b = 0

@[simp]

theorem Nat.mod_self (n : Nat) : n % n = 0

theorem Nat.mod_one (x : Nat) : x % 1 = 0

theorem Nat.div_add_mod (m : Nat) (n : Nat) : n * (m / n) + m % n = m

theorem Nat.div_eq_sub_div {b : Nat} {a : Nat} (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1

theorem Nat.mod_add_div (m : Nat) (k : Nat) : m % k + k * (m / k) = m

@[simp]

theorem Nat.div_one (n : Nat) : n / 1 = n

@[simp]

theorem Nat.div_zero (n : Nat) : n / 0 = 0

@[simp]

theorem Nat.zero_div (b : Nat) : 0 / b = 0

theorem Nat.le_div_iff_mul_le {k : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

theorem Nat.div_mul_le_self (m : Nat) (n : Nat) : m / n * n ≤ m

theorem Nat.div_lt_iff_lt_mul {k : Nat} {x : Nat} {y : Nat} (Hk : 0 < k) : x / k < y ↔ x < y * k

@[simp]

theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = Nat.succ (x / z)

@[simp]

theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = Nat.succ (x / z)

theorem Nat.add_mul_div_left (x : Nat) (z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

theorem Nat.add_mul_div_right (x : Nat) (y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y

@[simp]

theorem Nat.add_mod_right (x : Nat) (z : Nat) : (x + z) % z = x % z

@[simp]

theorem Nat.add_mod_left (x : Nat) (z : Nat) : (x + z) % x = z % x

@[simp]

theorem Nat.add_mul_mod_self_left (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % y = x % y

@[simp]

theorem Nat.add_mul_mod_self_right (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % z = x % z

@[simp]

theorem Nat.mul_mod_right (m : Nat) (n : Nat) : m * n % m = 0

@[simp]

theorem Nat.mul_mod_left (m : Nat) (n : Nat) : m * n % n = 0

theorem Nat.div_eq_of_lt_le {k : Nat} {n : Nat} {m : Nat} (lo : k * n ≤ m) (hi : m < Nat.succ k * n) : m / n = k

theorem Nat.sub_mul_div (x : Nat) (n : Nat) (p : Nat) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p

theorem Nat.mul_sub_div (x : Nat) (n : Nat) (p : Nat) (h₁ : x < n * p) : (n * p - Nat.succ x) / n = p - Nat.succ (x / n)

theorem Nat.mul_mod_mul_left (z : Nat) (x : Nat) (y : Nat) : z * x % (z * y) = z * (x % y)

theorem Nat.div_eq_of_lt {a : Nat} {b : Nat} (h₀ : a < b) : a / b = 0