Basic operations on the natural numbers

This file contains:

• some basic lemmas about natural numbers
• extra recursors:
  • leRecOn, le_induction: recursion and induction principles starting at non-zero numbers
  • decreasing_induction: recursion growing downwards
  • le_rec_on', decreasing_induction': versions with slightly weaker assumptions
  • strong_rec': recursion based on strong inequalities
• decidability instances on predicates about the natural numbers

Many theorems that used to live in this file have been moved to Data.Nat.Order, so that this file requires fewer imports. For each section here there is a corresponding section in that file with additional results. It may be possible to move some of these results here, by tweaking their proofs.

instance Nat.nontrivial : Nontrivial ℕ

Equations

• Nat.nontrivial = (_ : Nontrivial ℕ)

succ, pred

theorem Nat.succ_pos' {n : ℕ} : 0 < Nat.succ n

theorem Nat.succ_inj {a : ℕ} {b : ℕ} : Nat.succ a = Nat.succ b ↔ a = b

Alias of Nat.succ_inj'.

theorem Nat.succ_injective : Function.Injective Nat.succ

theorem Nat.succ_ne_succ {m : ℕ} {n : ℕ} : Nat.succ m ≠ Nat.succ n ↔ m ≠ n

theorem Nat.succ_succ_ne_one (n : ℕ) : Nat.succ (Nat.succ n) ≠ 1

@[simp]

theorem Nat.one_lt_succ_succ (n : ℕ) : 1 < Nat.succ (Nat.succ n)

theorem LT.lt.nat_succ_le {n : ℕ} {m : ℕ} (h : n < m) : Nat.succ n ≤ m

Alias of Nat.succ_le_of_lt.

theorem Nat.not_succ_lt_self {n : ℕ} : ¬Nat.succ n < n

theorem Nat.lt_succ_iff {m : ℕ} {n : ℕ} : m < Nat.succ n ↔ m ≤ n

theorem Nat.succ_le_iff {m : ℕ} {n : ℕ} : Nat.succ m ≤ n ↔ m < n

theorem Nat.le_succ_iff {m : ℕ} {n : ℕ} : m ≤ Nat.succ n ↔ m ≤ n ∨ m = Nat.succ n

theorem Nat.of_le_succ {m : ℕ} {n : ℕ} : m ≤ Nat.succ n → m ≤ n ∨ m = Nat.succ n

Alias of the forward direction of Nat.le_succ_iff.

theorem Nat.lt_succ_iff_lt_or_eq {m : ℕ} {n : ℕ} : m < Nat.succ n ↔ m < n ∨ m = n

theorem Nat.eq_of_lt_succ_of_not_lt {m : ℕ} {n : ℕ} (hmn : m < n + 1) (h : ¬m < n) : m = n

theorem Nat.eq_of_le_of_lt_succ {m : ℕ} {n : ℕ} (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n

theorem Nat.lt_iff_le_pred {m : ℕ} {n : ℕ} : 0 < n → (m < n ↔ m ≤ n - 1)

theorem Nat.le_of_pred_lt {n : ℕ} {m : ℕ} : Nat.pred m < n → m ≤ n

theorem Nat.lt_iff_add_one_le {m : ℕ} {n : ℕ} : m < n ↔ m + 1 ≤ n

theorem Nat.lt_add_one_iff {m : ℕ} {n : ℕ} : m < n + 1 ↔ m ≤ n

theorem Nat.lt_one_add_iff {m : ℕ} {n : ℕ} : m < 1 + n ↔ m ≤ n

theorem Nat.add_one_le_iff {m : ℕ} {n : ℕ} : m + 1 ≤ n ↔ m < n

theorem Nat.one_add_le_iff {m : ℕ} {n : ℕ} : 1 + m ≤ n ↔ m < n

theorem Nat.one_le_iff_ne_zero {n : ℕ} : 1 ≤ n ↔ n ≠ 0

theorem Nat.one_lt_iff_ne_zero_and_ne_one {n : ℕ} : 1 < n ↔ n ≠ 0 ∧ n ≠ 1

theorem Nat.le_one_iff_eq_zero_or_eq_one {n : ℕ} : n ≤ 1 ↔ n = 0 ∨ n = 1

theorem Nat.pred_eq_sub_one (n : ℕ) : Nat.pred n = n - 1

@[simp]

theorem Nat.pred_one_add (n : ℕ) : Nat.pred (1 + n) = n

This ensures that simp succeeds on pred (n + 1) = n.

theorem Nat.pred_eq_self_iff {n : ℕ} : Nat.pred n = n ↔ n = 0

theorem Nat.pred_eq_of_eq_succ {m : ℕ} {n : ℕ} (H : m = Nat.succ n) : Nat.pred m = n

@[simp]

theorem Nat.pred_eq_succ_iff {m : ℕ} {n : ℕ} : Nat.pred n = Nat.succ m ↔ n = m + 2

theorem Nat.and_forall_succ {p : ℕ → Prop} : (p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n

theorem Nat.or_exists_succ {p : ℕ → Prop} : (p 0 ∨ ∃ (n : ℕ), p (n + 1)) ↔ ∃ (n : ℕ), p n

theorem Nat.forall_lt_succ {n : ℕ} {p : ℕ → Prop} : (∀ (m : ℕ), m < n + 1 → p m) ↔ (∀ (m : ℕ), m < n → p m) ∧ p n

theorem Nat.exists_lt_succ {n : ℕ} {p : ℕ → Prop} : (∃ (m : ℕ), m < n + 1 ∧ p m) ↔ (∃ (m : ℕ), m < n ∧ p m) ∨ p n

theorem Nat.two_lt_of_ne {n : ℕ} : n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n

pred

@[simp]

theorem Nat.add_succ_sub_one (m : ℕ) (n : ℕ) : m + Nat.succ n - 1 = m + n

@[simp]

theorem Nat.succ_add_sub_one (n : ℕ) (m : ℕ) : Nat.succ m + n - 1 = m + n

theorem Nat.pred_sub (n : ℕ) (m : ℕ) : Nat.pred n - m = Nat.pred (n - m)

theorem Nat.self_add_sub_one (n : ℕ) : n + (n - 1) = 2 * n - 1

theorem Nat.sub_one_add_self (n : ℕ) : n - 1 + n = 2 * n - 1

theorem Nat.self_add_pred (n : ℕ) : n + Nat.pred n = Nat.pred (2 * n)

theorem Nat.pred_add_self (n : ℕ) : Nat.pred n + n = Nat.pred (2 * n)

add

@[simp]

theorem Nat.add_def {m : ℕ} {n : ℕ} : Nat.add m n = m + n

theorem Nat.exists_eq_add_of_le {m : ℕ} {n : ℕ} (h : m ≤ n) : ∃ (k : ℕ), n = m + k

theorem Nat.exists_eq_add_of_le' {m : ℕ} {n : ℕ} (h : m ≤ n) : ∃ (k : ℕ), n = k + m

theorem Nat.exists_eq_add_of_lt {m : ℕ} {n : ℕ} (h : m < n) : ∃ (k : ℕ), n = m + k + 1

mul

@[simp]

theorem Nat.mul_def {m : ℕ} {n : ℕ} : Nat.mul m n = m * n

theorem Nat.two_mul_ne_two_mul_add_one {m : ℕ} {n : ℕ} : 2 * n ≠ 2 * m + 1

theorem Nat.mul_left_inj {a : ℕ} {b : ℕ} {c : ℕ} (ha : a ≠ 0) : b * a = c * a ↔ b = c

theorem Nat.mul_right_inj {a : ℕ} {b : ℕ} {c : ℕ} (ha : a ≠ 0) : a * b = a * c ↔ b = c

theorem Nat.mul_ne_mul_left {a : ℕ} {b : ℕ} {c : ℕ} (ha : a ≠ 0) : b * a ≠ c * a ↔ b ≠ c

theorem Nat.mul_ne_mul_right {a : ℕ} {b : ℕ} {c : ℕ} (ha : a ≠ 0) : a * b ≠ a * c ↔ b ≠ c

theorem Nat.mul_eq_left {a : ℕ} {b : ℕ} (ha : a ≠ 0) : a * b = a ↔ b = 1

theorem Nat.mul_eq_right {a : ℕ} {b : ℕ} (hb : b ≠ 0) : a * b = b ↔ a = 1

theorem Nat.mul_right_eq_self_iff {a : ℕ} {b : ℕ} (ha : 0 < a) : a * b = a ↔ b = 1

theorem Nat.mul_left_eq_self_iff {a : ℕ} {b : ℕ} (hb : 0 < b) : a * b = b ↔ a = 1

theorem Nat.one_lt_mul_iff {m : ℕ} {n : ℕ} : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

The product of two natural numbers is greater than 1 if and only if at least one of them is greater than 1 and both are positive.

div

theorem Nat.div_le_iff_le_mul_add_pred {a : ℕ} {b : ℕ} {c : ℕ} (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1)

theorem Nat.div_lt_self' (a : ℕ) (b : ℕ) : (a + 1) / (b + 2) < a + 1

A version of Nat.div_lt_self using successors, rather than additional hypotheses.

theorem Nat.le_div_iff_mul_le' {a : ℕ} {b : ℕ} {c : ℕ} (hb : 0 < b) : a ≤ c / b ↔ a * b ≤ c

theorem Nat.div_lt_iff_lt_mul' {a : ℕ} {b : ℕ} {c : ℕ} (hb : 0 < b) : a / b < c ↔ a < c * b

theorem Nat.one_le_div_iff {a : ℕ} {b : ℕ} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

theorem Nat.div_lt_one_iff {a : ℕ} {b : ℕ} (hb : 0 < b) : a / b < 1 ↔ a < b

theorem Nat.div_le_div_right {a : ℕ} {b : ℕ} {c : ℕ} (h : a ≤ b) : a / c ≤ b / c

theorem Nat.lt_of_div_lt_div {a : ℕ} {b : ℕ} {c : ℕ} (h : a / c < b / c) : a < b

theorem Nat.div_pos {a : ℕ} {b : ℕ} (hba : b ≤ a) (hb : 0 < b) : 0 < a / b

theorem Nat.lt_mul_of_div_lt {a : ℕ} {b : ℕ} {c : ℕ} (h : a / c < b) (hc : 0 < c) : a < b * c

theorem Nat.mul_div_le_mul_div_assoc (a : ℕ) (b : ℕ) (c : ℕ) : a * (b / c) ≤ a * b / c

theorem Nat.eq_mul_of_div_eq_right {a : ℕ} {b : ℕ} {c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) : a = b * c

theorem Nat.div_eq_iff_eq_mul_right {a : ℕ} {b : ℕ} {c : ℕ} (H : 0 < b) (H' : b ∣ a) : a / b = c ↔ a = b * c

theorem Nat.div_eq_iff_eq_mul_left {a : ℕ} {b : ℕ} {c : ℕ} (H : 0 < b) (H' : b ∣ a) : a / b = c ↔ a = c * b

theorem Nat.eq_mul_of_div_eq_left {a : ℕ} {b : ℕ} {c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) : a = c * b

theorem Nat.mul_div_cancel_left' {a : ℕ} {b : ℕ} (Hd : a ∣ b) : a * (b / a) = b

theorem Nat.lt_div_mul_add {a : ℕ} {b : ℕ} (hb : 0 < b) : a < a / b * b + b

@[simp]

theorem Nat.div_left_inj {a : ℕ} {b : ℕ} {d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

theorem Nat.div_mul_div_comm {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} : b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)

theorem Nat.div_pow {a : ℕ} {b : ℕ} {c : ℕ} (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c

Recursion and induction principles

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

@[simp]

theorem Nat.rec_zero {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) : Nat.rec h0 h 0 = h0

@[simp]

theorem Nat.rec_add_one {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)

def Nat.leRecOn' {n : ℕ} {C : ℕ → Sort u_1} {m : ℕ} : n ≤ m → (⦃k : ℕ⦄ → n ≤ k → C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k ≥ n, there is a map from C n to each C m, n ≤ m.

Equations

• Nat.leRecOn' H x x_1 = Eq.recOn (_ : n = 0) x_1
• Nat.leRecOn' H x x_1 = Or.by_cases (_ : n ≤ m ∨ n = Nat.succ m) (fun (h : n ≤ m) => x h (Nat.leRecOn' h x x_1)) fun (h : n = m + 1) => Eq.recOn h x_1

def Nat.leRecOn {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} : n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k + 1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see Nat.leRecOn'.

Equations

• Nat.leRecOn H x x_1 = Eq.recOn (_ : n = 0) x_1
• Nat.leRecOn H x x_1 = Or.by_cases (_ : n ≤ m ∨ n = Nat.succ m) (fun (h : n ≤ m) => x (Nat.leRecOn h (fun {k : ℕ} => x) x_1)) fun (h : n = m + 1) => Eq.recOn h x_1

theorem Nat.leRecOn_self {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : Nat.leRecOn (_ : n ≤ n) (fun {k : ℕ} => next) x = x

theorem Nat.leRecOn_succ {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k : ℕ} => next) x)

theorem Nat.leRecOn_succ' {C : ℕ → Sort u_1} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : Nat.leRecOn h (fun {k : ℕ} => next) x = next x

theorem Nat.leRecOn_trans {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} {k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : Nat.leRecOn (_ : n ≤ k) next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)

theorem Nat.leRecOn_succ_left {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m) {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : Nat.leRecOn h2 (fun {k : ℕ} => next) (next x) = Nat.leRecOn h1 (fun {k : ℕ} => next) x

theorem Nat.leRecOn_injective {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Injective next) : Function.Injective (Nat.leRecOn hnm fun {k : ℕ} => next)

theorem Nat.leRecOn_surjective {C : ℕ → Sort u_1} {n : ℕ} {m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Surjective next) : Function.Surjective (Nat.leRecOn hnm fun {k : ℕ} => next)

def Nat.strongRec' {p : ℕ → Sort u_1} (H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n) (n : ℕ) : p n

Recursion principle based on <.

Equations

• Nat.strongRec' H x = H x fun (m : ℕ) (x : m < x) => Nat.strongRec' H m

def Nat.strongRecOn' {P : ℕ → Sort u_1} (n : ℕ) (h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n) : P n

Recursion principle based on < applied to some natural number.

Equations

• Nat.strongRecOn' n h = Nat.strongRec' h n

theorem Nat.strongRecOn'_beta {n : ℕ} {P : ℕ → Sort u_1} {h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n} : Nat.strongRecOn' n h = h n fun (m : ℕ) (x : m < n) => Nat.strongRecOn' m h

theorem Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m (_ : m ≤ m)) (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) (_ : m ≤ Nat.succ n)) (n : ℕ) (hmn : m ≤ n) : P n hmn

Induction principle starting at a non-zero number. For maps to a Sort* see leRecOn. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

def Nat.decreasingInduction {m : ℕ} {n : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (mn : m ≤ n) (hP : P n) : P m

Decreasing induction: if P (k+1) implies P k, then P n implies P m for all m ≤ n. Also works for functions to Sort*. For m version assuming only the assumption for k < n, see decreasing_induction'.

Equations

• Nat.decreasingInduction h mn hP = Nat.leRecOn mn (fun {k : ℕ} (ih : P k → P m) (hsk : P (k + 1)) => ih (h k hsk)) (fun (h : P m) => h) hP

@[simp]

theorem Nat.decreasingInduction_self {n : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (nn : n ≤ n) (hP : P n) : Nat.decreasingInduction h nn hP = hP

theorem Nat.decreasingInduction_succ {m : ℕ} {n : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (mn : m ≤ n) (msn : m ≤ n + 1) (hP : P (n + 1)) : Nat.decreasingInduction h msn hP = Nat.decreasingInduction h mn (h n hP)

@[simp]

theorem Nat.decreasingInduction_succ' {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) {m : ℕ} (msm : m ≤ m + 1) (hP : P (m + 1)) : Nat.decreasingInduction h msm hP = h m hP

theorem Nat.decreasingInduction_trans {m : ℕ} {n : ℕ} {k : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (hmn : m ≤ n) (hnk : n ≤ k) (hP : P k) : Nat.decreasingInduction h (_ : m ≤ k) hP = Nat.decreasingInduction h hmn (Nat.decreasingInduction h hnk hP)

theorem Nat.decreasingInduction_succ_left {m : ℕ} {n : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (smn : m + 1 ≤ n) (mn : m ≤ n) (hP : P n) : Nat.decreasingInduction h mn hP = h m (Nat.decreasingInduction h smn hP)

def Nat.strongSubRecursion {P : ℕ → ℕ → Sort u_1} (H : (m n : ℕ) → ((x y : ℕ) → x < m → y < n → P x y) → P m n) (n : ℕ) (m : ℕ) : P n m

Given P : ℕ → ℕ → Sort*, if for all m n : ℕ we can extend P from the rectangle strictly below (m, n) to P m n, then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

Equations

• Nat.strongSubRecursion H x✝ x = H x✝ x fun (x_1 y : ℕ) (x_2 : x_1 < x✝) (x : y < x) => Nat.strongSubRecursion H x_1 y

def Nat.pincerRecursion {P : ℕ → ℕ → Sort u_1} (Ha0 : (m : ℕ) → P m 0) (H0b : (n : ℕ) → P 0 n) (H : (x y : ℕ) → P x (Nat.succ y) → P (Nat.succ x) y → P (Nat.succ x) (Nat.succ y)) (n : ℕ) (m : ℕ) : P n m

Given P : ℕ → ℕ → Sort*, if we have P m 0 and P 0 n for all m n : ℕ, and for any m n : ℕ we can extend P from (m, n + 1) and (m + 1, n) to (m + 1, n + 1) then we have P m n for all m n : ℕ.

Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

Equations

• Nat.pincerRecursion Ha0 H0b H x 0 = Ha0 x
• Nat.pincerRecursion Ha0 H0b H 0 x = H0b x
• Nat.pincerRecursion Ha0 H0b H (Nat.succ m) (Nat.succ n) = H m n (Nat.pincerRecursion Ha0 H0b H m (Nat.succ n)) (Nat.pincerRecursion Ha0 H0b H (Nat.succ m) n)

def Nat.decreasingInduction' {P : ℕ → Sort u_1} {m : ℕ} {n : ℕ} (h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) (mn : m ≤ n) (hP : P n) : P m

Decreasing induction: if P (k+1) implies P k for all m ≤ k < n, then P n implies P m. Also works for functions to Sort*. Weakens the assumptions of decreasing_induction.

Equations

• One or more equations did not get rendered due to their size.

mod, dvd

theorem Nat.mod_eq_iff_lt {m : ℕ} {n : ℕ} (hn : n ≠ 0) : m % n = m ↔ m < n

@[simp]

theorem Nat.mod_succ_eq_iff_lt {m : ℕ} {n : ℕ} : m % Nat.succ n = m ↔ m < Nat.succ n

@[simp]

theorem Nat.mod_succ (n : ℕ) : n % Nat.succ n = n

theorem Nat.mod_add_div' (a : ℕ) (b : ℕ) : a % b + a / b * b = a

theorem Nat.div_add_mod' (a : ℕ) (b : ℕ) : a / b * b + a % b = a

theorem Nat.div_mod_unique {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h : 0 < b) : a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b

See also Nat.divModEquiv for a similar statement as an Equiv.

theorem Nat.dvd_add_left {a : ℕ} {b : ℕ} {c : ℕ} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b

theorem Nat.dvd_add_right {a : ℕ} {b : ℕ} {c : ℕ} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c

theorem Nat.mul_dvd_mul_iff_left {a : ℕ} {b : ℕ} {c : ℕ} (ha : 0 < a) : a * b ∣ a * c ↔ b ∣ c

theorem Nat.mul_dvd_mul_iff_right {a : ℕ} {b : ℕ} {c : ℕ} (hc : 0 < c) : a * c ∣ b * c ↔ a ∣ b

@[simp]

theorem Nat.mod_mod_of_dvd {b : ℕ} {c : ℕ} (a : ℕ) (h : c ∣ b) : a % b % c = a % c

theorem Nat.add_mod_eq_add_mod_right {a : ℕ} {b : ℕ} {d : ℕ} (c : ℕ) (H : a % d = b % d) : (a + c) % d = (b + c) % d

theorem Nat.add_mod_eq_add_mod_left {a : ℕ} {b : ℕ} {d : ℕ} (c : ℕ) (H : a % d = b % d) : (c + a) % d = (c + b) % d

theorem Nat.mul_dvd_of_dvd_div {a : ℕ} {b : ℕ} {c : ℕ} (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b

theorem Nat.eq_of_dvd_of_div_eq_one {a : ℕ} {b : ℕ} (hab : a ∣ b) (h : b / a = 1) : a = b

theorem Nat.eq_zero_of_dvd_of_div_eq_zero {a : ℕ} {b : ℕ} (hab : a ∣ b) (h : b / a = 0) : b = 0

theorem Nat.div_le_div_left {a : ℕ} {b : ℕ} {c : ℕ} (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c

theorem Nat.lt_mul_div_succ {b : ℕ} (a : ℕ) (hb : 0 < b) : a < b * (a / b + 1)

theorem Nat.mul_add_mod' (a : ℕ) (b : ℕ) (c : ℕ) : (a * b + c) % b = c % b

theorem Nat.mul_add_mod_of_lt {a : ℕ} {b : ℕ} {c : ℕ} (h : c < b) : (a * b + c) % b = c

find

theorem Nat.find_eq_iff {m : ℕ} {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

@[simp]

theorem Nat.find_lt_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : Nat.find h < n ↔ ∃ (m : ℕ), m < n ∧ p m

@[simp]

theorem Nat.find_le_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ (m : ℕ), m ≤ n ∧ p m

@[simp]

theorem Nat.le_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m

@[simp]

theorem Nat.lt_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m

@[simp]

theorem Nat.find_eq_zero {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : Nat.find h = 0 ↔ p 0

theorem Nat.find_mono {p : ℕ → Prop} {q : ℕ → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ℕ), q n → p n) {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} : Nat.find hp ≤ Nat.find hq

theorem Nat.find_le {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {h : ∃ (n : ℕ), p n} (hn : p n) : Nat.find h ≤ n

theorem Nat.find_comp_succ {p : ℕ → Prop} [DecidablePred p] (h₁ : ∃ (n : ℕ), p n) (h₂ : ∃ (n : ℕ), p (n + 1)) (h0 : ¬p 0) : Nat.find h₁ = Nat.find h₂ + 1

find_greatest

def Nat.findGreatest (P : ℕ → Prop) [DecidablePred P] : ℕ → ℕ

find_greatest P n is the largest i ≤ bound such that P i holds, or 0 if no such i exists

Equations

• Nat.findGreatest P 0 = 0
• Nat.findGreatest P (Nat.succ n) = if P (n + 1) then n + 1 else Nat.findGreatest P n

@[simp]

theorem Nat.findGreatest_zero {P : ℕ → Prop} [DecidablePred P] : Nat.findGreatest P 0 = 0

theorem Nat.findGreatest_succ {P : ℕ → Prop} [DecidablePred P] (n : ℕ) : Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n

@[simp]

theorem Nat.findGreatest_eq {P : ℕ → Prop} [DecidablePred P] {n : ℕ} : P n → Nat.findGreatest P n = n

@[simp]

theorem Nat.findGreatest_of_not {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : ¬P (n + 1)) : Nat.findGreatest P (n + 1) = Nat.findGreatest P n

Decidability of predicates

instance Nat.decidableBallLT (n : ℕ) (P : (k : ℕ) → k < n → Prop) [(n_1 : ℕ) → (h : n_1 < n) → Decidable (P n_1 h)] : Decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)

Equations

• One or more equations did not get rendered due to their size.
• Nat.decidableBallLT 0 x_3 = isTrue (_ : ∀ (x : ℕ) (x_1 : x < 0), x_3 x x_1)

instance Nat.decidableForallFin {n : ℕ} (P : Fin n → Prop) [DecidablePred P] : Decidable (∀ (i : Fin n), P i)

Equations

• Nat.decidableForallFin P = decidable_of_iff (∀ (k : ℕ) (h : k < n), P { val := k, isLt := h }) (_ : (∀ (k : ℕ) (h : k < n), P { val := k, isLt := h }) ↔ ∀ (i : Fin n), P i)

instance Nat.decidableBallLe (n : ℕ) (P : (k : ℕ) → k ≤ n → Prop) [(n_1 : ℕ) → (h : n_1 ≤ n) → Decidable (P n_1 h)] : Decidable (∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)

Equations

• Nat.decidableBallLe n P = decidable_of_iff (∀ (k : ℕ) (h : k < Nat.succ n), P k (_ : k ≤ n)) (_ : (∀ (k : ℕ) (h : k < Nat.succ n), P k (_ : k ≤ n)) ↔ ∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)

instance Nat.decidableExistsLT {p : ℕ → Prop} [h : DecidablePred p] : DecidablePred fun (n : ℕ) => ∃ (m : ℕ), m < n ∧ p m

Equations

• Nat.decidableExistsLT 0 = isFalse (_ : ¬∃ (x : ℕ), x < 0 ∧ p x)
• Nat.decidableExistsLT (Nat.succ n) = decidable_of_decidable_of_iff (_ : (∃ (m : ℕ), m < n ∧ p m) ∨ p n ↔ ∃ (x : ℕ), x < Nat.succ n ∧ p x)

instance Nat.decidableExistsLe {p : ℕ → Prop} [DecidablePred p] : DecidablePred fun (n : ℕ) => ∃ (m : ℕ), m ≤ n ∧ p m

Equations

• Nat.decidableExistsLe n = decidable_of_iff (∃ (m : ℕ), m < n + 1 ∧ p m) (_ : (∃ (a : ℕ), a < n + 1 ∧ p a) ↔ ∃ (a : ℕ), a ≤ n ∧ p a)