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.Batteries?) for lemmas that could go to Batteries
• Data.Nat.Basic for the lemmas that require mathlib definitions

instance Nat.instLinearOrder : LinearOrder ℕ

Equations

• Nat.instLinearOrder = LinearOrder.mk Nat.le_total inferInstance inferInstance inferInstance Nat.instLinearOrder.proof_1 Nat.instLinearOrder.proof_2 Nat.instLinearOrder.proof_3

instance Nat.instPreorder : Preorder ℕ

Equations

• Nat.instPreorder = inferInstance

instance Nat.instPartialOrder : PartialOrder ℕ

Equations

• Nat.instPartialOrder = inferInstance

instance Nat.instMin_mathlib : Min ℕ

Equations

• Nat.instMin_mathlib = inferInstance

instance Nat.instMax_mathlib : Max ℕ

Equations

• Nat.instMax_mathlib = inferInstance

instance Nat.instOrd_mathlib : Ord ℕ

Equations

• Nat.instOrd_mathlib = inferInstance

instance Nat.instNontrivial : Nontrivial ℕ

@[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_injective : Function.Injective succ

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

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.pow_eq_self_iff {a b : ℕ} (ha : 1 < a) : a ^ b = a ↔ b = 1

For a > 1, a ^ b = a iff b = 1.

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

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 (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 (leRecOn hnm fun {k : ℕ} => next)

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

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

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

theorem Nat.dvd_sub' {m n k : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - 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.dvd_left_injective : Function.Injective fun (x1 x2 : ℕ) => x1 ∣ x2

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

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) ⋯