# 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
Equations
@[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.succm 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 < nm 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
@[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_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.and_forall_succ {p : } :
(p 0 ∀ (n : ), p (n + 1)) ∀ (n : ), p n
theorem Nat.or_exists_succ {p : } :
(p 0 ∃ (n : ), p (n + 1)) ∃ (n : ), p n
theorem Nat.forall_lt_succ {n : } {p : } :
(∀ (m : ), m < n + 1p m) (∀ (m : ), m < np m) p n
theorem Nat.exists_lt_succ {n : } {p : } :
(∃ (m : ), m < n + 1 p m) (∃ (m : ), m < n p m) p n
theorem Nat.two_lt_of_ne {n : } :
n 0n 1n 22 < 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_def {m : } {n : } :
m.add 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 - 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 ba + 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 ad ca / 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)
@[deprecated Nat.mul_div_mul_comm]
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)

Alias of Nat.mul_div_mul_comm.

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_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 0a ^ 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
@[deprecated Nat.pow_lt_pow_left]
theorem Nat.pow_lt_pow_of_lt_left {a : } {b : } (h : a < b) {n : } :
n 0a ^ n < b ^ n

Alias of Nat.pow_lt_pow_left.

@[deprecated Nat.pow_le_pow_iff_left]
theorem Nat.pow_le_iff_le_left {a : } {b : } {n : } (hn : n 0) :
a ^ n b ^ n a b

Alias of Nat.pow_le_pow_iff_left.

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.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 nC (n + 1)) :
Nat.rec h0 h 0 = h0
theorem Nat.rec_add_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) (n : ) :
Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
@[simp]
theorem Nat.rec_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) :
Nat.rec h0 h 1 = h 0 h0
def Nat.leRec {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (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.
Instances For
@[simp]
theorem Nat.leRec_self {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
Nat.leRec refl le_succ_of_le = refl
@[simp]
theorem Nat.leRec_succ {m : } {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (h1 : n m) {h2 : n m + 1} :
Nat.leRec refl le_succ_of_le h2 = le_succ_of_le h1 (Nat.leRec refl le_succ_of_le h1)
theorem Nat.leRec_succ' {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
Nat.leRec refl le_succ_of_le = le_succ_of_le refl
theorem Nat.leRec_trans {n : } {m : } {k : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (hnm : n m) (hmk : m k) :
Nat.leRec refl le_succ_of_le = Nat.leRec (Nat.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 mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) {m : } (h1 : n m) (h2 : n + 1 m) :
Nat.leRec (le_succ_of_le refl) (fun (k : ) (h : n + 1 k) (ih : motive k ) => le_succ_of_le ih) h2 = Nat.leRec refl le_succ_of_le h1
@[deprecated Nat.leRec]
def Nat.leRecOn' {n : } {C : Sort u_1} {m : } :
n m(k : ⦄ → n kC kC (k + 1))C nC 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.

Prefer Nat.leRec, which can be used as induction h using Nat.leRec.

Equations
Instances For
def Nat.leRecOn {C : Sort u_1} {n : } {m : } :
n m({k : } → C kC (k + 1))C nC 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
Instances For
theorem Nat.leRecOn_self {C : Sort u_1} {n : } {next : {k : } → C kC (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 kC (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 kC (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 kC (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 : } {next : {k : } → C kC (k + 1)} (x : C n) (h1 : n m) (h2 : n + 1 m) :
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 kC (k + 1)) (Hnext : ∀ (n : ), ) :
Function.Injective (Nat.leRecOn hnm fun {k : } => next)
theorem Nat.leRecOn_surjective {C : Sort u_1} {n : } {m : } (hnm : n m) (next : {k : } → C kC (k + 1)) (Hnext : ∀ (n : ), ) :
Function.Surjective (Nat.leRecOn hnm fun {k : } => next)
@[irreducible]
def Nat.strongRec' {p : Sort u_1} (H : (n : ) → ((m : ) → m < np m)p n) (n : ) :
p n

Recursion principle based on <.

Equations
• = H x fun (m : ) (x : m < x) =>
Instances For
def Nat.strongRecOn' {P : Sort u_1} (n : ) (h : (n : ) → ((m : ) → m < nP m)P n) :
P n

Recursion principle based on < applied to some natural number.

Equations
• n.strongRecOn' h =
Instances For
theorem Nat.strongRecOn'_beta {n : } {P : Sort u_1} {h : (n : ) → ((m : ) → m < nP m)P n} :
n.strongRecOn' h = h n fun (m : ) (x : m < n) => m.strongRecOn' h
theorem Nat.le_induction {m : } {P : (n : ) → m nProp} (base : P m ) (succ : ∀ (n : ) (hmn : m n), P n hmnP (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.decreasingInduction {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive 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.
Instances For
@[simp]
theorem Nat.decreasingInduction_self {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) :
Nat.decreasingInduction of_succ self = self
theorem Nat.decreasingInduction_succ {m : } {n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) (mn : m n) (msn : m n + 1) :
Nat.decreasingInduction of_succ self msn = Nat.decreasingInduction (fun (i : ) (hi : i < n) => of_succ i ) (of_succ n self) mn
@[simp]
theorem Nat.decreasingInduction_succ' {n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) :
Nat.decreasingInduction of_succ self = of_succ n self
theorem Nat.decreasingInduction_trans {m : } {n : } {k : } {motive : (m : ) → m kSort u_1} (hmn : m n) (hnk : n k) (of_succ : (k_1 : ) → (h : k_1 < k) → motive (k_1 + 1) hmotive k_1 ) (self : motive k ) :
Nat.decreasingInduction of_succ self = Nat.decreasingInduction (fun (n_1 : ) (ih : n_1 < n) => of_succ n_1 ) (Nat.decreasingInduction of_succ self hnk) hmn
theorem Nat.decreasingInduction_succ_left {m : } {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) (smn : m + 1 n) (mn : m n) :
Nat.decreasingInduction of_succ self mn = of_succ m smn (Nat.decreasingInduction of_succ self smn)
@[irreducible]
def Nat.strongSubRecursion {P : Sort u_1} (H : (m n : ) → ((x y : ) → x < my < nP 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
• = H x✝ x fun (x_1 y : ) (x_2 : x_1 < x✝) (x : y < x) =>
Instances For
@[irreducible]
def Nat.pincerRecursion {P : Sort u_1} (Ha0 : (m : ) → P m 0) (H0b : (n : ) → P 0 n) (H : (x y : ) → P x y.succP x.succ yP 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
Instances For
def Nat.decreasingInduction' {m : } {n : } {P : Sort u_1} (h : (k : ) → k < nm kP (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.
Instances For
@[irreducible]
theorem Nat.diag_induction (P : Prop) (ha : ∀ (a : ), P (a + 1) (a + 1)) (hb : ∀ (b : ), P 0 (b + 1)) (hd : ∀ (a b : ), a < bP (a + 1) bP a (b + 1)P (a + 1) (b + 1)) (a : ) (b : ) :
a < bP 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 : } (hk : k S) (h_ind : ∀ (k : ), k Sk + 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 : } (hb : 0 S) (h_ind : ∀ (k : ), k Sk + 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_ne_one {n : } :
¬n % 2 = 1 n % 2 = 0
@[simp]
theorem Nat.mod_two_ne_zero {n : } :
¬n % 2 = 0 n % 2 = 1
@[deprecated Nat.mod_mul_right_div_self]
theorem Nat.div_mod_eq_mod_mul_div (a : ) (b : ) (c : ) :
a / b % c = a % (b * c) / b
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.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
@[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 < a1 < 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_of_ne_one {n : } :
n 11 % 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 dk 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
@[deprecated Nat.dvd_div_iff_mul_dvd]
theorem Nat.dvd_div_iff {a : } {b : } {c : } (hbc : c b) :
a b / c c * a b

Alias of Nat.dvd_div_iff_mul_dvd.

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 an ba 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)).

@[irreducible]
theorem Nat.sqrt.iter_sq_le (n : ) (guess : ) :
Nat.sqrt.iter n guess * Nat.sqrt.iter n guess n
@[irreducible]
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 : ) :
n.sqrt * n.sqrt n
theorem Nat.sqrt_le' (n : ) :
n.sqrt ^ 2 n
theorem Nat.lt_succ_sqrt (n : ) :
n < n.sqrt.succ * n.sqrt.succ
theorem Nat.lt_succ_sqrt' (n : ) :
n < n.sqrt.succ ^ 2
theorem Nat.sqrt_le_add (n : ) :
n n.sqrt * n.sqrt + n.sqrt + n.sqrt
theorem Nat.le_sqrt {m : } {n : } :
m n.sqrt m * m n
theorem Nat.le_sqrt' {m : } {n : } :
m n.sqrt m ^ 2 n
theorem Nat.sqrt_lt {m : } {n : } :
m.sqrt < n m < n * n
theorem Nat.sqrt_lt' {m : } {n : } :
m.sqrt < n m < n ^ 2
theorem Nat.sqrt_le_self (n : ) :
n.sqrt n
theorem Nat.sqrt_le_sqrt {m : } {n : } (h : m n) :
m.sqrt n.sqrt
@[simp]
theorem Nat.sqrt_zero :
= 0
@[simp]
theorem Nat.sqrt_one :
= 1
theorem Nat.sqrt_eq_zero {n : } :
n.sqrt = 0 n = 0
theorem Nat.eq_sqrt {a : } {n : } :
a = n.sqrt a * a n n < (a + 1) * (a + 1)
theorem Nat.eq_sqrt' {a : } {n : } :
a = n.sqrt a ^ 2 n n < (a + 1) ^ 2
theorem Nat.le_three_of_sqrt_eq_one {n : } (h : n.sqrt = 1) :
n 3
theorem Nat.sqrt_lt_self {n : } (h : 1 < n) :
n.sqrt < n
theorem Nat.sqrt_pos {n : } :
0 < n.sqrt 0 < n
theorem Nat.sqrt_add_eq {a : } (n : ) (h : a n + n) :
(n * n + a).sqrt = n
theorem Nat.sqrt_add_eq' {a : } (n : ) (h : a n + n) :
(n ^ 2 + a).sqrt = n
theorem Nat.sqrt_eq (n : ) :
(n * n).sqrt = n
theorem Nat.sqrt_eq' (n : ) :
(n ^ 2).sqrt = n
theorem Nat.sqrt_succ_le_succ_sqrt (n : ) :
n.succ.sqrt n.sqrt.succ
theorem Nat.exists_mul_self (x : ) :
(∃ (n : ), n * n = x) x.sqrt * x.sqrt = x
theorem Nat.exists_mul_self' (x : ) :
(∃ (n : ), n ^ 2 = x) x.sqrt ^ 2 = x
theorem Nat.sqrt_mul_sqrt_lt_succ (n : ) :
n.sqrt * n.sqrt < n + 1
theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ) :
n.sqrt ^ 2 < n + 1
theorem Nat.succ_le_succ_sqrt (n : ) :
n + 1 (n.sqrt + 1) * (n.sqrt + 1)
theorem Nat.succ_le_succ_sqrt' (n : ) :
n + 1 (n.sqrt + 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 < nn < (m + 1) ^ 2¬∃ (t : ), t ^ 2 = n

### Decidability of predicates #

instance Nat.decidableLoHi (lo : ) (hi : ) (P : ) [H : ] :
Decidable (∀ (x : ), lo xx < hiP x)
Equations
instance Nat.decidableLoHiLe (lo : ) (hi : ) (P : ) [] :
Decidable (∀ (x : ), lo xx hiP x)
Equations