mathlib docs: core.init.data.nat.lemmas

n.strong_rec_on h = (λ (this : Π (n m : ℕ), m < n → p m), this n.succ n _) (λ (n : ℕ), nat.rec (λ (m : ℕ) (h₁ : m < 0), absurd h₁ _) (λ (n : ℕ) (ih : Π (m : ℕ), m < n → p m) (m : ℕ) (h₁ : m < n.succ), _.by_cases (λ (a : m < n), ih m a) (λ (a : m = n), eq.rec (λ (h₁ : n < n.succ), h n ih) _ h₁)) n)

source

theorem nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) :

(∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) → p n

source

theorem nat.case_strong_induction_on {p : ℕ → Prop} (a : ℕ) :

p 0 → (∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p n.succ) → p a

source

theorem nat.mod_def (x y : ℕ) :

x % y = ite (0 < y ∧ y ≤ x) ((x - y) % y) x

source

@[simp]

theorem nat.mod_zero (a : ℕ) :

a % 0 = a

source

theorem nat.mod_eq_of_lt {a b : ℕ} :

a < b → a % b = a

source

@[simp]

theorem nat.zero_mod (b : ℕ) :

0 % b = 0

source

theorem nat.mod_eq_sub_mod {a b : ℕ} :

a ≥ b → a % b = (a - b) % b

source

theorem nat.mod_lt (x : ℕ) {y : ℕ} :

y > 0 → x % y < y

source

@[simp]

theorem nat.mod_self (n : ℕ) :

n % n = 0

source

@[simp]

theorem nat.mod_one (n : ℕ) :

n % 1 = 0

source

theorem nat.mod_two_eq_zero_or_one (n : ℕ) :

n % 2 = 0 ∨ n % 2 = 1

source

theorem nat.div_def (x y : ℕ) :

x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0

source

theorem nat.mod_add_div (m k : ℕ) :

m % k + k * (m / k) = m

source

@[simp]

theorem nat.div_one (n : ℕ) :

n / 1 = n

source

@[simp]

theorem nat.div_zero (n : ℕ) :

n / 0 = 0

source

@[simp]

theorem nat.zero_div (b : ℕ) :

0 / b = 0

source

theorem nat.div_le_of_le_mul {m n k : ℕ} :

m ≤ k * n → m / k ≤ n

source

theorem nat.div_le_self (m n : ℕ) :

m / n ≤ m

source

theorem nat.div_eq_sub_div {a b : ℕ} :

b > 0 → a ≥ b → a / b = (a - b) / b + 1

source

theorem nat.div_eq_of_lt {a b : ℕ} :

a < b → a / b = 0

source

theorem nat.le_div_iff_mul_le (x y : ℕ) {k : ℕ} :

k > 0 → (x ≤ y / k ↔ x * k ≤ y)

source

theorem nat.div_lt_iff_lt_mul (x y : ℕ) {k : ℕ} :

k > 0 → (x / k < y ↔ x < y * k)

source

def nat.iterate {α : Sort u} :

(α → α) → ℕ → α → α

Equations

op^[k.succ ] a = op^[k] (op a)
op^[0] a = a

source

theorem nat.add_one_ne_zero (n : ℕ) :

n + 1 ≠ 0

source

theorem nat.eq_zero_or_eq_succ_pred (n : ℕ) :

n = 0 ∨ n = n.pred.succ

source

theorem nat.exists_eq_succ_of_ne_zero {n : ℕ} :

n ≠ 0 → (∃ (k : ℕ), n = k.succ)

source

theorem nat.discriminate {B : Sort u} {n : ℕ} :

(n = 0 → B) → (Π (m : ℕ), n = m.succ → B) → B

source

theorem nat.one_succ_zero :

1 = 1

source

theorem nat.two_step_induction {P : ℕ → Sort u} (H1 : P 0) (H2 : P 1) (H3 : Π (n : ℕ), P n → P n.succ → P n.succ.succ) (a : ℕ) :

P a

source

theorem nat.sub_induction {P : ℕ → ℕ → Sort u} (H1 : Π (m : ℕ), P 0 m) (H2 : Π (n : ℕ), P n.succ 0) (H3 : Π (n m : ℕ), P n m → P n.succ m.succ) (n m : ℕ) :

P n m

source

theorem nat.succ_add_eq_succ_add (n m : ℕ) :

n.succ + m = n + m.succ

source

theorem nat.add_right_comm (n m k : ℕ) :

n + m + k = n + k + m

source

theorem nat.eq_zero_of_add_eq_zero {n m : ℕ} :

n + m = 0 → n = 0 ∧ m = 0

source

theorem nat.eq_zero_of_mul_eq_zero {n m : ℕ} :

n * m = 0 → n = 0 ∨ m = 0

source

theorem nat.le_succ_of_pred_le {n m : ℕ} :

n.pred ≤ m → n ≤ m.succ

source

theorem nat.le_lt_antisymm {n m : ℕ} :

n ≤ m → m < n → false

source

theorem nat.lt_le_antisymm {n m : ℕ} :

n < m → m ≤ n → false

source

theorem nat.lt_asymm {n m : ℕ} :

n < m → ¬m < n

source

def nat.lt_ge_by_cases {a b : ℕ} {C : Sort u} :

(a < b → C) → (a ≥ b → C) → C

Equations

nat.lt_ge_by_cases h₁ h₂ = decidable.by_cases h₁ (λ (h : ¬a < b), h₂ _)

source

def nat.lt_by_cases {a b : ℕ} {C : Sort u} :

(a < b → C) → (a = b → C) → (b < a → C) → C

Equations

nat.lt_by_cases h₁ h₂ h₃ = nat.lt_ge_by_cases h₁ (λ (h₁ : a ≥ b), nat.lt_ge_by_cases h₃ (λ (h : b ≥ a), h₂ _))

source

theorem nat.lt_trichotomy (a b : ℕ) :

a < b ∨ a = b ∨ b < a

source

theorem nat.eq_or_lt_of_not_lt {a b : ℕ} :

¬a < b → a = b ∨ b < a

source

theorem nat.lt_succ_of_lt {a b : ℕ} :

a < b → a < b.succ

source

def nat.one_pos :

0 < 1

Equations

nat.one_pos = nat.zero_lt_one

source

theorem nat.sub_le_sub_left {n m : ℕ} (k : ℕ) :

n ≤ m → k - m ≤ k - n

source

theorem nat.succ_sub_sub_succ (n m k : ℕ) :

n.succ - m - k.succ = n - m - k

source

theorem nat.sub.right_comm (m n k : ℕ) :

m - n - k = m - k - n

source

theorem nat.mul_pred_left (n m : ℕ) :

n.pred * m = n * m - m

source

theorem nat.mul_pred_right (n m : ℕ) :

n * m.pred = n * m - n

source

theorem nat.mul_sub_right_distrib (n m k : ℕ) :

(n - m) * k = n * k - m * k

source

theorem nat.mul_sub_left_distrib (n m k : ℕ) :

n * (m - k) = n * m - n * k

source

theorem nat.mul_self_sub_mul_self_eq (a b : ℕ) :

a * a - b * b = (a + b) * (a - b)

source

theorem nat.succ_mul_succ_eq (a b : ℕ) :

a.succ * b.succ = a * b + a + b + 1

source

theorem nat.succ_sub {m n : ℕ} :

m ≥ n → m.succ - n = (m - n).succ

source

theorem nat.sub_pos_of_lt {m n : ℕ} :

m < n → n - m > 0

source

theorem nat.sub_sub_self {n m : ℕ} :

m ≤ n → n - (n - m) = m

source

theorem nat.sub_add_comm {n m k : ℕ} :

k ≤ n → n + m - k = n - k + m

source

theorem nat.sub_one_sub_lt {n i : ℕ} :

i < n → n - 1 - i < n

source

theorem nat.pred_inj {a b : ℕ} :

a > 0 → b > 0 → a.pred = b.pred → a = b

source

def nat.find_x {p : ℕ → Prop} [decidable_pred p] :

(∃ (n : ℕ), p n) → {n // p n ∧ ∀ (m : ℕ), m < n → ¬p m}

Equations

nat.find_x H = _.fix (λ (m : ℕ) (IH : Π (y : ℕ), lbp y m → (λ (k : ℕ), (∀ (n : ℕ), n < k → ¬p n) → {n // p n ∧ ∀ (m : ℕ), m < n → ¬p m}) y) (al : ∀ (n : ℕ), n < m → ¬p n), dite (p m) (λ (pm : p m), ⟨m, _⟩) (λ (pm : ¬p m), have this : ∀ (n : ℕ), n ≤ m → ¬p n, from _, IH (m + 1) _ _)) 0 nat.find_x._proof_5