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

See note [foundational algebra order theory].

TODO

Split this file into:

• Data.Nat.Init (or maybe Data.Nat.Std?) for lemmas that could go to Std
• Data.Nat.Basic for the lemmas that require mathlib definitions

instance Nat.instNontrivial : Nontrivial ℕ

Equations

• Nat.instNontrivial = ⋯

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.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_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

@[simp]

theorem Nat.lt_one_iff {n : ℕ} : n < 1 ↔ n = 0

theorem Nat.one_le_of_lt {a : ℕ} {b : ℕ} (h : a < b) : 1 ≤ b

@[simp]

theorem Nat.min_eq_zero_iff {m : ℕ} {n : ℕ} : min m n = 0 ↔ m = 0 ∨ n = 0

@[simp]

theorem Nat.max_eq_zero_iff {m : ℕ} {n : ℕ} : max m n = 0 ↔ m = 0 ∧ n = 0

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)

theorem Nat.pred_le_iff {m : ℕ} {n : ℕ} : Nat.pred m ≤ n ↔ m ≤ Nat.succ n

theorem Nat.lt_of_lt_pred {m : ℕ} {n : ℕ} (h : m < n - 1) : m < n

theorem Nat.le_add_pred_of_pos {b : ℕ} (a : ℕ) (hb : b ≠ 0) : a ≤ b + (a - 1)

add

@[simp]

theorem Nat.add_left_inj {m : ℕ} {k : ℕ} {n : ℕ} : m + n = k + n ↔ m = k

Alias of Nat.add_right_cancel_iff.

@[simp]

theorem Nat.add_right_inj {m : ℕ} {k : ℕ} {n : ℕ} : n + m = n + k ↔ m = k

Alias of Nat.add_left_cancel_iff.

@[simp]

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

@[simp]

theorem Nat.add_eq_left {a : ℕ} {b : ℕ} : a + b = a ↔ b = 0

@[simp]

theorem Nat.add_eq_right {a : ℕ} {b : ℕ} : a + b = b ↔ a = 0

theorem Nat.two_le_iff (n : ℕ) : 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1

theorem Nat.add_eq_max_iff {m : ℕ} {n : ℕ} : m + n = max m n ↔ m = 0 ∨ n = 0

theorem Nat.add_eq_min_iff {m : ℕ} {n : ℕ} : m + n = min m n ↔ m = 0 ∧ n = 0

@[simp]

theorem Nat.add_eq_zero {m : ℕ} {n : ℕ} : m + n = 0 ↔ m = 0 ∧ n = 0

theorem Nat.add_pos_iff_pos_or_pos {m : ℕ} {n : ℕ} : 0 < m + n ↔ 0 < m ∨ 0 < n

theorem Nat.add_eq_one_iff {m : ℕ} {n : ℕ} : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

theorem Nat.add_eq_two_iff {m : ℕ} {n : ℕ} : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

theorem Nat.add_eq_three_iff {m : ℕ} {n : ℕ} : m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

theorem Nat.le_add_one_iff {m : ℕ} {n : ℕ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Nat.le_and_le_add_one_iff {m : ℕ} {n : ℕ} : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

theorem Nat.add_succ_lt_add {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hab : a < b) (hcd : c < d) : a + c + 1 < b + d

theorem Nat.le_or_le_of_add_eq_add_pred {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c

sub

theorem Nat.sub_succ' (m : ℕ) (n : ℕ) : m - Nat.succ n = m - n - 1

A version of Nat.sub_succ in the form _ - 1 instead of Nat.pred _.

theorem Nat.sub_eq_of_eq_add' {a : ℕ} {b : ℕ} {c : ℕ} (h : a = b + c) : a - b = c

theorem Nat.eq_sub_of_add_eq {a : ℕ} {b : ℕ} {c : ℕ} (h : c + b = a) : c = a - b

theorem Nat.eq_sub_of_add_eq' {a : ℕ} {b : ℕ} {c : ℕ} (h : b + c = a) : c = a - b

theorem Nat.lt_sub_iff_add_lt {a : ℕ} {b : ℕ} {c : ℕ} : a < c - b ↔ a + b < c

theorem Nat.lt_sub_iff_add_lt' {a : ℕ} {b : ℕ} {c : ℕ} : a < c - b ↔ b + a < c

theorem Nat.sub_lt_iff_lt_add {a : ℕ} {b : ℕ} {c : ℕ} (hba : b ≤ a) : a - b < c ↔ a < b + c

theorem Nat.sub_lt_iff_lt_add' {a : ℕ} {b : ℕ} {c : ℕ} (hba : b ≤ a) : a - b < c ↔ a < c + b

theorem Nat.sub_sub_sub_cancel_right {a : ℕ} {b : ℕ} {c : ℕ} (h : c ≤ b) : a - c - (b - c) = a - b

theorem Nat.add_sub_sub_cancel {a : ℕ} {b : ℕ} {c : ℕ} (h : c ≤ a) : a + b - (a - c) = b + c

theorem Nat.sub_add_sub_cancel {a : ℕ} {b : ℕ} {c : ℕ} (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

theorem Nat.lt_pred_iff {a : ℕ} {b : ℕ} : a < Nat.pred b ↔ Nat.succ a < b

theorem Nat.sub_lt_sub_iff_right {a : ℕ} {b : ℕ} {c : ℕ} (h : c ≤ a) : a - c < b - c ↔ a < b

mul

@[simp]

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

theorem Nat.zero_eq_mul {m : ℕ} {n : ℕ} : 0 = m * n ↔ m = 0 ∨ n = 0

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.le_of_mul_le_mul_right {a : ℕ} {b : ℕ} {c : ℕ} (h : a * c ≤ b * c) (hc : 0 < c) : a ≤ b

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.

theorem Nat.eq_one_of_mul_eq_one_right {m : ℕ} {n : ℕ} (H : m * n = 1) : m = 1

theorem Nat.eq_one_of_mul_eq_one_left {m : ℕ} {n : ℕ} (H : m * n = 1) : n = 1

@[simp]

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

@[simp]

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

theorem Nat.eq_zero_of_double_le {n : ℕ} (h : 2 * n ≤ n) : n = 0

theorem Nat.eq_zero_of_mul_le {m : ℕ} {n : ℕ} (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0

theorem Nat.succ_mul_pos {n : ℕ} (m : ℕ) (hn : 0 < n) : 0 < Nat.succ m * n

theorem Nat.mul_self_le_mul_self {m : ℕ} {n : ℕ} (h : m ≤ n) : m * m ≤ n * n

theorem Nat.mul_lt_mul'' {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hac : a < c) (hbd : b < d) : a * b < c * d

theorem Nat.mul_self_lt_mul_self {m : ℕ} {n : ℕ} (h : m < n) : m * m < n * n

theorem Nat.mul_self_le_mul_self_iff {m : ℕ} {n : ℕ} : m * m ≤ n * n ↔ m ≤ n

theorem Nat.mul_self_lt_mul_self_iff {m : ℕ} {n : ℕ} : m * m < n * n ↔ m < n

theorem Nat.le_mul_self (n : ℕ) : n ≤ n * n

theorem Nat.mul_self_inj {m : ℕ} {n : ℕ} : m * m = n * n ↔ m = n

@[simp]

theorem Nat.lt_mul_self_iff {n : ℕ} : n < n * n ↔ 1 < n

theorem Nat.add_sub_one_le_mul {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b

theorem Nat.add_le_mul {a : ℕ} (ha : 2 ≤ a) {b : ℕ} : 2 ≤ b → a + b ≤ a * b

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_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.eq_zero_of_le_div {m : ℕ} {n : ℕ} (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0

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

theorem Nat.eq_zero_of_le_half {n : ℕ} (h : n ≤ n / 2) : n = 0

theorem Nat.le_half_of_half_lt_sub {a : ℕ} {b : ℕ} (h : a / 2 < a - b) : b ≤ a / 2

theorem Nat.half_le_of_sub_le_half {a : ℕ} {b : ℕ} (h : a - b ≤ a / 2) : a / 2 ≤ b

theorem Nat.div_le_of_le_mul' {m : ℕ} {n : ℕ} {k : ℕ} (h : m ≤ k * n) : m / k ≤ n

theorem Nat.div_le_self' (m : ℕ) (n : ℕ) : m / n ≤ m

theorem Nat.two_mul_odd_div_two {n : ℕ} (hn : n % 2 = 1) : 2 * (n / 2) = n - 1

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

theorem Nat.div_eq_self {m : ℕ} {n : ℕ} : m / n = m ↔ m = 0 ∨ n = 1

theorem Nat.div_eq_sub_mod_div {m : ℕ} {n : ℕ} : m / n = (m - m % n) / n

theorem Nat.eq_div_of_mul_eq_left {a : ℕ} {b : ℕ} {c : ℕ} (hc : c ≠ 0) (h : a * c = b) : a = b / c

theorem Nat.eq_div_of_mul_eq_right {a : ℕ} {b : ℕ} {c : ℕ} (hc : c ≠ 0) (h : c * a = b) : a = b / c

theorem Nat.mul_le_of_le_div (k : ℕ) (x : ℕ) (y : ℕ) (h : x ≤ y / k) : x * k ≤ y

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

pow

TODO

• Rename Nat.pow_le_pow_of_le_left to Nat.pow_le_pow_left, protect it, remove the alias
• Rename Nat.pow_le_pow_of_le_right to Nat.pow_le_pow_right, protect it, remove the alias

theorem Nat.pow_lt_pow_left {a : ℕ} {b : ℕ} (h : a < b) {n : ℕ} : n ≠ 0 → a ^ n < b ^ n

theorem Nat.pow_lt_pow_right {a : ℕ} {m : ℕ} {n : ℕ} (ha : 1 < a) (h : m < n) : a ^ m < a ^ n

theorem Nat.pow_le_pow_iff_left {a : ℕ} {b : ℕ} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem Nat.pow_lt_pow_iff_left {a : ℕ} {b : ℕ} {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

theorem Nat.pow_left_injective {n : ℕ} (hn : n ≠ 0) : Function.Injective fun (a : ℕ) => a ^ n

theorem Nat.pow_right_injective {a : ℕ} (ha : 2 ≤ a) : Function.Injective fun (x : ℕ) => a ^ x

@[simp]

theorem Nat.pow_eq_zero {a : ℕ} {n : ℕ} : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

theorem Nat.le_self_pow {n : ℕ} (hn : n ≠ 0) (a : ℕ) : a ≤ a ^ n

theorem Nat.lt_pow_self {a : ℕ} (ha : 1 < a) (n : ℕ) : n < a ^ n

theorem Nat.lt_two_pow (n : ℕ) : n < 2 ^ n

theorem Nat.one_le_pow (n : ℕ) (m : ℕ) (h : 0 < m) : 1 ≤ m ^ n

theorem Nat.one_le_pow' (n : ℕ) (m : ℕ) : 1 ≤ (m + 1) ^ n

theorem Nat.one_lt_pow {a : ℕ} {n : ℕ} (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n

theorem Nat.two_pow_succ (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n

theorem Nat.one_lt_pow' (n : ℕ) (m : ℕ) : 1 < (m + 2) ^ (n + 1)

@[simp]

theorem Nat.one_lt_pow_iff {n : ℕ} (hn : n ≠ 0) {a : ℕ} : 1 < a ^ n ↔ 1 < a

theorem Nat.one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1)

theorem Nat.mul_lt_mul_pow_succ {a : ℕ} {b : ℕ} {n : ℕ} (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)

theorem Nat.sq_sub_sq (a : ℕ) (b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem Nat.pow_two_sub_pow_two (a : ℕ) (b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of Nat.sq_sub_sq.

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 ⋯ x_1
• Nat.leRecOn' H x x_1 = Or.by_cases ⋯ (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 ⋯ x_1
• Nat.leRecOn H x x_1 = Or.by_cases ⋯ (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 ⋯ (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 ⋯ 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 ⋯) (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) (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 ⋯ 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' {m : ℕ} {n : ℕ} {P : ℕ → Sort u_1} (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.

theorem Nat.diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ (a : ℕ), P (a + 1) (a + 1)) (hb : ∀ (b : ℕ), P 0 (b + 1)) (hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) (a : ℕ) (b : ℕ) : a < b → P a b

Given a predicate on two naturals P : ℕ → ℕ → Prop, P a b is true for all a < b if P (a + 1) (a + 1) is true for all a, P 0 (b + 1) is true for all b and for all a < b, P (a + 1) b is true and P a (b + 1) is true implies P (a + 1) (b + 1) is true.

theorem Nat.set_induction_bounded {n : ℕ} {k : ℕ} {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (hnk : k ≤ n) : n ∈ S

A subset of ℕ containing k : ℕ and closed under Nat.succ contains every n ≥ k.

theorem Nat.set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (n : ℕ) : n ∈ S

A subset of ℕ containing zero and closed under Nat.succ contains all of ℕ.

mod, dvd

theorem Nat.lt_div_iff_mul_lt {d : ℕ} {n : ℕ} (hdn : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n

theorem Nat.mul_div_eq_iff_dvd {n : ℕ} {d : ℕ} : d * (n / d) = n ↔ d ∣ n

theorem Nat.mul_div_lt_iff_not_dvd {d : ℕ} {n : ℕ} : d * (n / d) < n ↔ ¬d ∣ n

theorem Nat.div_eq_iff_eq_of_dvd_dvd {a : ℕ} {b : ℕ} {n : ℕ} (hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b

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

theorem Nat.div_ne_zero_iff {a : ℕ} {b : ℕ} (hb : b ≠ 0) : a / b ≠ 0 ↔ b ≤ a

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

theorem Nat.mul_div_mul_comm_of_dvd_dvd {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / d)

@[simp]

theorem Nat.mul_mod_mod (a : ℕ) (b : ℕ) (c : ℕ) : a * (b % c) % c = a * b % c

@[simp]

theorem Nat.mod_mul_mod (a : ℕ) (b : ℕ) (c : ℕ) : a % c * b % c = a * b % c

theorem Nat.pow_mod (a : ℕ) (b : ℕ) (n : ℕ) : a ^ b % n = (a % n) ^ b % n

theorem Nat.not_pos_pow_dvd {a : ℕ} {n : ℕ} : 1 < a → 1 < n → ¬a ^ n ∣ a

theorem Nat.lt_of_pow_dvd_right {a : ℕ} {b : ℕ} {n : ℕ} (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b

theorem Nat.div_dvd_of_dvd {m : ℕ} {n : ℕ} (h : n ∣ m) : m / n ∣ m

theorem Nat.div_div_self {m : ℕ} {n : ℕ} (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n

theorem Nat.not_dvd_of_pos_of_lt {m : ℕ} {n : ℕ} (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n

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.sub_mod_eq_zero_of_mod_eq {m : ℕ} {n : ℕ} {k : ℕ} (h : m % k = n % k) : (m - n) % k = 0

If m and n are equal mod k, m - n is zero mod k.

@[simp]

theorem Nat.one_mod (n : ℕ) : 1 % (n + 2) = 1

theorem Nat.one_mod_of_ne_one {n : ℕ} : n ≠ 1 → 1 % n = 1

theorem Nat.dvd_sub_mod {n : ℕ} (k : ℕ) : n ∣ k - k % n

theorem Nat.add_mod_eq_ite {m : ℕ} {n : ℕ} {k : ℕ} : (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k

theorem Nat.not_dvd_of_between_consec_multiples {m : ℕ} {n : ℕ} {k : ℕ} (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m

m is not divisible by n if it is between n * k and n * (k + 1) for some k.

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

special case of mul_dvd_mul_iff_left for ℕ. Duplicated here to keep simple imports for this file.

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

special case of mul_dvd_mul_iff_right for ℕ. Duplicated here to keep simple imports for this file.

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 {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d

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

@[simp]

theorem Nat.not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ bit1 n

@[simp]

theorem Nat.dvd_add_self_left {m : ℕ} {n : ℕ} : m ∣ m + n ↔ m ∣ n

A natural number m divides the sum m + n if and only if m divides n.

@[simp]

theorem Nat.dvd_add_self_right {m : ℕ} {n : ℕ} : m ∣ n + m ↔ m ∣ n

A natural number m divides the sum n + m if and only if m divides n.

theorem Nat.dvd_sub' {m : ℕ} {n : ℕ} {k : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n

theorem Nat.succ_div (a : ℕ) (b : ℕ) : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0

theorem Nat.succ_div_of_dvd {a : ℕ} {b : ℕ} (hba : b ∣ a + 1) : (a + 1) / b = a / b + 1

theorem Nat.succ_div_of_not_dvd {a : ℕ} {b : ℕ} (hba : ¬b ∣ a + 1) : (a + 1) / b = a / b

theorem Nat.dvd_iff_div_mul_eq (n : ℕ) (d : ℕ) : d ∣ n ↔ n / d * d = n

theorem Nat.dvd_iff_le_div_mul (n : ℕ) (d : ℕ) : d ∣ n ↔ n ≤ n / d * d

theorem Nat.dvd_iff_dvd_dvd (n : ℕ) (d : ℕ) : d ∣ n ↔ ∀ (k : ℕ), k ∣ d → k ∣ n

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

@[simp]

theorem Nat.dvd_div_iff {a : ℕ} {b : ℕ} {c : ℕ} (hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b

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

@[simp]

theorem Nat.div_dvd_iff_dvd_mul {a : ℕ} {b : ℕ} {c : ℕ} (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c

@[simp]

theorem Nat.div_div_div_eq_div {a : ℕ} {b : ℕ} {c : ℕ} (dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a

theorem Nat.eq_zero_of_dvd_of_lt {a : ℕ} {b : ℕ} (w : a ∣ b) (h : b < a) : b = 0

If a small natural number is divisible by a larger natural number, the small number is zero.

theorem Nat.le_of_lt_add_of_dvd {a : ℕ} {b : ℕ} {n : ℕ} (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b

theorem Nat.not_dvd_iff_between_consec_multiples (n : ℕ) {a : ℕ} (ha : 0 < a) : (∃ (k : ℕ), a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n

n is not divisible by a iff it is between a * k and a * (k + 1) for some k.

theorem Nat.dvd_right_iff_eq {m : ℕ} {n : ℕ} : (∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n

Two natural numbers are equal if and only if they have the same multiples.

theorem Nat.dvd_left_iff_eq {m : ℕ} {n : ℕ} : (∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n

Two natural numbers are equal if and only if they have the same divisors.

theorem Nat.dvd_left_injective : Function.Injective fun (x x_1 : ℕ) => x ∣ x_1

dvd is injective in the left argument

theorem Nat.div_lt_div_of_lt_of_dvd {a : ℕ} {b : ℕ} {d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d

sqrt

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).

theorem Nat.sqrt.iter_sq_le (n : ℕ) (guess : ℕ) : Nat.sqrt.iter n guess * Nat.sqrt.iter n guess ≤ n

theorem Nat.sqrt.lt_iter_succ_sq (n : ℕ) (guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) : n < (Nat.sqrt.iter n guess + 1) * (Nat.sqrt.iter n guess + 1)

theorem Nat.sqrt_le (n : ℕ) : Nat.sqrt n * Nat.sqrt n ≤ n

theorem Nat.sqrt_le' (n : ℕ) : Nat.sqrt n ^ 2 ≤ n

theorem Nat.lt_succ_sqrt (n : ℕ) : n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)

theorem Nat.lt_succ_sqrt' (n : ℕ) : n < Nat.succ (Nat.sqrt n) ^ 2

theorem Nat.sqrt_le_add (n : ℕ) : n ≤ Nat.sqrt n * Nat.sqrt n + Nat.sqrt n + Nat.sqrt n

theorem Nat.le_sqrt {m : ℕ} {n : ℕ} : m ≤ Nat.sqrt n ↔ m * m ≤ n

theorem Nat.le_sqrt' {m : ℕ} {n : ℕ} : m ≤ Nat.sqrt n ↔ m ^ 2 ≤ n

theorem Nat.sqrt_lt {m : ℕ} {n : ℕ} : Nat.sqrt m < n ↔ m < n * n

theorem Nat.sqrt_lt' {m : ℕ} {n : ℕ} : Nat.sqrt m < n ↔ m < n ^ 2

theorem Nat.sqrt_le_self (n : ℕ) : Nat.sqrt n ≤ n

theorem Nat.sqrt_le_sqrt {m : ℕ} {n : ℕ} (h : m ≤ n) : Nat.sqrt m ≤ Nat.sqrt n

@[simp]

theorem Nat.sqrt_zero : Nat.sqrt 0 = 0

@[simp]

theorem Nat.sqrt_one : Nat.sqrt 1 = 1

theorem Nat.sqrt_eq_zero {n : ℕ} : Nat.sqrt n = 0 ↔ n = 0

theorem Nat.eq_sqrt {a : ℕ} {n : ℕ} : a = Nat.sqrt n ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)

theorem Nat.eq_sqrt' {a : ℕ} {n : ℕ} : a = Nat.sqrt n ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

theorem Nat.le_three_of_sqrt_eq_one {n : ℕ} (h : Nat.sqrt n = 1) : n ≤ 3

theorem Nat.sqrt_lt_self {n : ℕ} (h : 1 < n) : Nat.sqrt n < n

theorem Nat.sqrt_pos {n : ℕ} : 0 < Nat.sqrt n ↔ 0 < n

theorem Nat.sqrt_add_eq {a : ℕ} (n : ℕ) (h : a ≤ n + n) : Nat.sqrt (n * n + a) = n

theorem Nat.sqrt_add_eq' {a : ℕ} (n : ℕ) (h : a ≤ n + n) : Nat.sqrt (n ^ 2 + a) = n

theorem Nat.sqrt_eq (n : ℕ) : Nat.sqrt (n * n) = n

theorem Nat.sqrt_eq' (n : ℕ) : Nat.sqrt (n ^ 2) = n

theorem Nat.sqrt_succ_le_succ_sqrt (n : ℕ) : Nat.sqrt (Nat.succ n) ≤ Nat.succ (Nat.sqrt n)

theorem Nat.exists_mul_self (x : ℕ) : (∃ (n : ℕ), n * n = x) ↔ Nat.sqrt x * Nat.sqrt x = x

theorem Nat.exists_mul_self' (x : ℕ) : (∃ (n : ℕ), n ^ 2 = x) ↔ Nat.sqrt x ^ 2 = x

theorem Nat.sqrt_mul_sqrt_lt_succ (n : ℕ) : Nat.sqrt n * Nat.sqrt n < n + 1

theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ℕ) : Nat.sqrt n ^ 2 < n + 1

theorem Nat.succ_le_succ_sqrt (n : ℕ) : n + 1 ≤ (Nat.sqrt n + 1) * (Nat.sqrt n + 1)

theorem Nat.succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (Nat.sqrt n + 1) ^ 2

theorem Nat.not_exists_sq {m : ℕ} {n : ℕ} (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ (t : ℕ), t * t = n

There are no perfect squares strictly between m² and (m+1)²

theorem Nat.not_exists_sq' {m : ℕ} {n : ℕ} : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ (t : ℕ), t ^ 2 = n

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

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

theorem Nat.find_add {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {hₘ : ∃ (m : ℕ), p (m + n)} {hₙ : ∃ (n : ℕ), p n} (hn : n ≤ Nat.find hₙ) : Nat.find hₘ + n = Nat.find hₙ

Nat.findGreatest

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

Nat.findGreatest 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

theorem Nat.findGreatest_eq_iff {m : ℕ} {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

theorem Nat.findGreatest_eq_zero_iff {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

@[simp]

theorem Nat.findGreatest_pos {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : 0 < Nat.findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

theorem Nat.findGreatest_spec {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n)

theorem Nat.findGreatest_le {P : ℕ → Prop} [DecidablePred P] (n : ℕ) : Nat.findGreatest P n ≤ n

theorem Nat.le_findGreatest {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n

theorem Nat.findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m : ℕ} {n : ℕ} (hmn : m ≤ n) : Nat.findGreatest P m ≤ Nat.findGreatest P n

theorem Nat.findGreatest_mono_left {P : ℕ → Prop} {Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (n : ℕ) : Nat.findGreatest P n ≤ Nat.findGreatest Q n

theorem Nat.findGreatest_mono {m : ℕ} {P : ℕ → Prop} {Q : ℕ → Prop} [DecidablePred P] {n : ℕ} [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (hmn : m ≤ n) : Nat.findGreatest P m ≤ Nat.findGreatest Q n

theorem Nat.findGreatest_is_greatest {k : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k

theorem Nat.findGreatest_of_ne_zero {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m

Decidability of predicates

instance Nat.decidableLoHi (lo : ℕ) (hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] : Decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)

Equations

• Nat.decidableLoHi lo hi P = decidable_of_iff (∀ (x : ℕ), x < hi - lo → P (lo + x)) ⋯

instance Nat.decidableLoHiLe (lo : ℕ) (hi : ℕ) (P : ℕ → Prop) [DecidablePred P] : Decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)

Equations

• Nat.decidableLoHiLe lo hi P = decidable_of_iff (∀ (x : ℕ), lo ≤ x → x < hi + 1 → P x) ⋯