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

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

instance Nat.instModNat : Mod Nat

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