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

This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries easily.

See note [foundational algebra order theory].

@[simp]

theorem Nat.default_eq_zero : default = 0

succ, pred

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

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

Alias of Nat.succ_inj'.

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

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

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

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

Alias of Nat.succ_le_of_lt.

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

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

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

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

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 : ℕ} : m.pred < n → m ≤ n

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

theorem Nat.lt_one_add_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.one_le_of_lt {a b : ℕ} (h : a < b) : 1 ≤ b

theorem Nat.min_left_comm (a b c : ℕ) : min a (min b c) = min b (min a c)

theorem Nat.max_left_comm (a b c : ℕ) : max a (max b c) = max b (max a c)

theorem Nat.min_right_comm (a b c : ℕ) : min (min a b) c = min (min a c) b

theorem Nat.max_right_comm (a b c : ℕ) : max (max a b) c = max (max a c) 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_one_add (n : ℕ) : (1 + n).pred = n

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

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

@[simp]

theorem Nat.pred_eq_succ_iff {m n : ℕ} : n - 1 = m + 1 ↔ n = m + 2

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 + n.succ - 1 = m + n

@[simp]

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

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

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 + n.pred = (2 * n).pred

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

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

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_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 - n.succ = 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 < b.pred ↔ a.succ < 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 : ℕ} : m.mul 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.mul_sub (n m k : ℕ) : n * (m - k) = n * m - n * k

Alias of Nat.mul_sub_left_distrib.

theorem Nat.sub_mul (n m k : ℕ) : (n - m) * k = n * k - m * k

Alias of Nat.mul_sub_right_distrib.

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 < m.succ * 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.le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

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.

@[deprecated Nat.le_div_iff_mul_le (since := "2024-11-06")]

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

@[deprecated Nat.div_lt_iff_lt_mul (since := "2024-11-06")]

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

@[simp]

theorem Nat.div_eq_zero_iff {a b : ℕ} : a / b = 0 ↔ b = 0 ∨ a < b

theorem Nat.div_ne_zero_iff {a b : ℕ} : a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a

@[simp]

theorem Nat.div_pos_iff {a b : ℕ} : 0 < a / b ↔ 0 < b ∧ b ≤ a

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.mul_div_mul_comm {a b c d : ℕ} (hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / 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_div_of_mul_le_mul {a b c d : ℕ} (hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) : a / b ≤ c / d

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

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

@[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.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

theorem Nat.pow_pos_iff {a n : ℕ} : 0 < a ^ n ↔ 0 < a ∨ n = 0

theorem Nat.pow_self_pos {n : ℕ} : 0 < n ^ n

theorem Nat.pow_self_mul_pow_self_le {m n : ℕ} : m ^ m * n ^ n ≤ (m + n) ^ (m + n)

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)) : rec h0 h 0 = h0

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

@[simp]

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

def Nat.leRec {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) {m : ℕ} (h : n ≤ m) : motive m h

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.

This is a version of Nat.le.rec that works for Sort u. Similarly to Nat.le.rec, it can be used as

induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry

Equations

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

theorem Nat.leRec_eq_leRec : @leRec = @le.rec

@[simp]

theorem Nat.leRec_self {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) : leRec refl le_succ_of_le ⋯ = refl

@[simp]

theorem Nat.leRec_succ {m n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (h1 : n ≤ m) {h2 : n ≤ m + 1} : leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)

theorem Nat.leRec_succ' {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) : leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

theorem Nat.leRec_trans {n m k : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (hnm : n ≤ m) (hmk : m ≤ k) : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun (x : ℕ) (h : n ≤ x) => le_succ_of_le h) hnm) (fun (x : ℕ) (h : m ≤ x) => le_succ_of_le ⋯) hmk

theorem Nat.leRec_succ_left {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) {m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m) : leRec (le_succ_of_le ⋯ refl) (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x ⋯) => le_succ_of_le ⋯ ih) h2 = leRec refl le_succ_of_le h1

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

Equations

• Nat.leRecOn h of_succ self = Nat.leRec self (fun (x : ℕ) (x_1 : n ≤ x) => of_succ) h

theorem Nat.leRecOn_self {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) : 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) : leRecOn h2 next x = next (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) : 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) : leRecOn ⋯ next x = leRecOn hmk next (leRecOn hnm next x)

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

@[irreducible]

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

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

theorem Nat.strongRecOn'_beta {n : ℕ} {P : ℕ → Sort u_1} {h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n} : n.strongRecOn' h = h n fun (m : ℕ) (x : m < n) => m.strongRecOn' 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. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

This is an alias of Nat.leRec, specialized to Prop.

def Nat.twoStepInduction {P : ℕ → Sort u_1} (zero : P 0) (one : P 1) (more : (n : ℕ) → P n → P (n + 1) → P (n + 2)) (a : ℕ) : P a

Induction principle deriving the next case from the two previous ones.

Equations

• Nat.twoStepInduction zero one more 0 = zero
• Nat.twoStepInduction zero one more 1 = one
• Nat.twoStepInduction zero one more n.succ.succ = more n (Nat.twoStepInduction zero one more n) (Nat.twoStepInduction zero one more (n + 1))

theorem Nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) : p n

theorem Nat.case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p (n + 1)) : p a

def Nat.decreasingInduction {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) {m : ℕ} (mn : m ≤ n) : motive m mn

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

For a version also assuming m ≤ k, see Nat.decreasingInduction'.

Equations

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

@[simp]

theorem Nat.decreasingInduction_self {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) : decreasingInduction of_succ self ⋯ = self

theorem Nat.decreasingInduction_succ {m n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯) (self : motive (n + 1) ⋯) (mn : m ≤ n) (msn : m ≤ n + 1) : decreasingInduction of_succ self msn = decreasingInduction (fun (x : ℕ) (x_1 : x < n) => of_succ x ⋯) (of_succ n ⋯ self) mn

@[simp]

theorem Nat.decreasingInduction_succ' {n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯) (self : motive (n + 1) ⋯) : decreasingInduction of_succ self ⋯ = of_succ n ⋯ self

theorem Nat.decreasingInduction_trans {m n k : ℕ} {motive : (m : ℕ) → m ≤ k → Sort u_1} (hmn : m ≤ n) (hnk : n ≤ k) (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive k ⋯) : decreasingInduction of_succ self ⋯ = decreasingInduction (fun (x : ℕ) (x_1 : x < n) => of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn

theorem Nat.decreasingInduction_succ_left {m n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) (smn : m + 1 ≤ n) (mn : m ≤ n) : decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)

@[irreducible]

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 y : ℕ) (x_1 : x < x✝¹) (x_2 : y < x✝) => Nat.strongSubRecursion H x y

@[irreducible]

def Nat.pincerRecursion {P : ℕ → ℕ → Sort u_1} (Ha0 : (m : ℕ) → P m 0) (H0b : (n : ℕ) → P 0 n) (H : (x y : ℕ) → P x y.succ → P x.succ y → P x.succ y.succ) (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 n.succ n_1.succ = H n n_1 (Nat.pincerRecursion Ha0 H0b H n n_1.succ) (Nat.pincerRecursion Ha0 H0b H n.succ n_1)

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

Equations

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

@[irreducible]

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.

mod, dvd

@[simp]

theorem Nat.mod_two_not_eq_one {n : ℕ} : ¬n % 2 = 1 ↔ n % 2 = 0

@[simp]

theorem Nat.mod_two_not_eq_zero {n : ℕ} : ¬n % 2 = 0 ↔ n % 2 = 1

theorem Nat.mod_two_ne_one {n : ℕ} : n % 2 ≠ 1 ↔ n % 2 = 0

theorem Nat.mod_two_ne_zero {n : ℕ} : n % 2 ≠ 0 ↔ n % 2 = 1

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

Variant of Nat.lt_div_iff_mul_lt that assumes d ∣ 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.le_iff_ne_zero_of_dvd {a b : ℕ} (ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0

theorem Nat.div_ne_zero_iff_of_dvd {a b : ℕ} (hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

@[simp]

theorem Nat.mul_mod_mod (a b c : ℕ) : a * (b % c) % 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.eq_of_dvd_of_lt_two_mul {a b : ℕ} (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b

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 % n.succ = m ↔ m < n.succ

@[simp]

theorem Nat.mod_succ (n : ℕ) : n % n.succ = 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_eq_one {n : ℕ} : 1 % n = 1 ↔ n ≠ 1

@[deprecated "No deprecation message was provided." (since := "2024-08-28")]

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 ∣ 2 * n + 1

@[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.

@[irreducible]

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_mul_dvd {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.div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d

Decidability of predicates

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

Equations

• lo.decidableLoHi 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

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