Documentation

Mathlib.Data.Nat.Defs

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

Implementation note #

Std has a home-baked development of the algebraic and order theoretic theory of ℕ which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...). This home-baked development is pursued in this file.

Less basic uses of ℕ should however use the typeclass-mediated development. Data.Nat.Basic gives access to the algebraic instances. Data.Nat.Order.Basic is the one giving access to the algebraic order instances.

TODO #

The names of this file, Data.Nat.Basic and Data.Nat.Order.Basic are archaic and don't match up with reality anymore. Rename them.

instance Nat.nontrivial :

Equations

Nat.nontrivial = ⋯

`succ`, `pred` #

theorem Nat.succ_pos' {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) :

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

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

`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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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)

Instances For

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

P m

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

Equations

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

Instances For

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.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) :

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

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

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

a * c ∣ b * c ↔ a ∣ b

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

`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

Instances For

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