data.nat.basic

# Basic operations on the natural numbers #

This file contains:

• instances on the natural numbers
• some basic lemmas about natural numbers
• extra recursors:
• `le_rec_on`, `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

### instances #

@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Extra instances to short-circuit type class resolution

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.monoid  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.distrib  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.subtype.order_bot (s : set ) [decidable_pred (λ (_x : ), _x s)] [h : nonempty s] :
Equations
@[protected, instance]
Equations
theorem nat.subtype.coe_bot {s : set } [decidable_pred (λ (_x : ), _x s)] [h : nonempty s] :
@[protected]
theorem nat.nsmul_eq_mul (m n : ) :
m n = m * n
theorem nat.eq_of_mul_eq_mul_right {n m k : } (Hm : 0 < m) (H : n * m = k * m) :
n = k
@[protected, instance]
Equations

### Recursion and `set.range`#

theorem nat.range_of_succ {α : Type u_1} (f : → α) :
theorem nat.range_rec {α : Type u_1} (x : α) (f : α → α) :
set.range (λ (n : ), nat.rec x f n) = {x} set.range (λ (n : ), nat.rec (f 0 x) (f nat.succ) n)
theorem nat.range_cases_on {α : Type u_1} (x : α) (f : → α) :
set.range (λ (n : ), n.cases_on x f) = {x}

### The units of the natural numbers as a `monoid` and `add_monoid`#

theorem nat.units_eq_one (u : ˣ) :
u = 1
u = 0
@[protected, simp]
theorem nat.is_unit_iff {n : } :
n = 1
@[protected, instance]
Equations
@[protected, instance]
Equations

### Equalities and inequalities involving zero and one #

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
@[protected]
theorem nat.mul_ne_zero {n m : } (n0 : n 0) (m0 : m 0) :
n * m 0
@[protected, simp]
theorem nat.mul_eq_zero {a b : } :
a * b = 0 a = 0 b = 0
@[protected, simp]
theorem nat.zero_eq_mul {a b : } :
0 = a * b a = 0 b = 0
theorem nat.eq_zero_of_double_le {a : } (h : 2 * a a) :
a = 0
theorem nat.eq_zero_of_mul_le {a b : } (hb : 2 b) (h : b * a a) :
a = 0
theorem nat.zero_max {m : } :
= m
@[simp]
theorem nat.min_eq_zero_iff {m n : } :
= 0 m = 0 n = 0
@[simp]
theorem nat.max_eq_zero_iff {m n : } :
= 0 m = 0 n = 0
theorem nat.add_eq_max_iff {n m : } :
n + m = n = 0 m = 0
theorem nat.add_eq_min_iff {n m : } :
n + m = n = 0 m = 0
theorem nat.one_le_of_lt {n m : } (h : n < m) :
1 m
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

### `succ`#

theorem has_lt.lt.nat_succ_le {n m : } (h : n < m) :
n.succ m
theorem nat.succ_eq_one_add (n : ) :
n.succ = 1 + n
theorem nat.eq_of_lt_succ_of_not_lt {a b : } (h1 : a < b + 1) (h2 : ¬a < b) :
a = b
theorem nat.eq_of_le_of_lt_succ {n m : } (h₁ : n m) (h₂ : m < n + 1) :
m = n
theorem nat.one_add (n : ) :
1 + n = n.succ
@[simp]
theorem nat.succ_pos' {n : } :
0 < n.succ
theorem nat.succ_inj' {n m : } :
n.succ = m.succ n = m
theorem nat.succ_ne_succ {n m : } :
n.succ m.succ n m
@[simp]
theorem nat.succ_succ_ne_one (n : ) :
@[simp]
theorem nat.one_lt_succ_succ (n : ) :
1 < n.succ.succ
theorem nat.two_le_iff (n : ) :
2 n n 0 n 1
theorem nat.succ_le_succ_iff {m n : } :
m.succ n.succ m n
theorem nat.max_succ_succ {m n : } :
= n).succ
theorem nat.not_succ_lt_self {n : } :
¬n.succ < n
theorem nat.lt_succ_iff {m n : } :
m < n.succ m n
theorem nat.succ_le_iff {m n : } :
m.succ n m < n
theorem nat.lt_iff_add_one_le {m n : } :
m < n m + 1 n
theorem nat.lt_add_one_iff {a b : } :
a < b + 1 a b
theorem nat.lt_one_add_iff {a b : } :
a < 1 + b a b
theorem nat.add_one_le_iff {a b : } :
a + 1 b a < b
theorem nat.one_add_le_iff {a b : } :
1 + a b a < b
theorem nat.of_le_succ {n m : } (H : n m.succ) :
n m n = m.succ
theorem nat.succ_lt_succ_iff {m n : } :
m.succ < n.succ m < n
@[simp]
theorem nat.lt_one_iff {n : } :
n < 1 n = 0
theorem nat.div_le_iff_le_mul_add_pred {m n k : } (n0 : 0 < n) :
m / n k m n * k + (n - 1)
theorem nat.two_lt_of_ne {n : } :
n 0n 1n 22 < n
theorem nat.forall_lt_succ {P : → Prop} {n : } :
(∀ (m : ), m < n.succP m) (∀ (m : ), m < nP m) P n
theorem nat.exists_lt_succ {P : → Prop} {n : } :
(∃ (m : ) (H : m < n.succ), P m) (∃ (m : ) (H : m < n), P m) P n

### `add`#

@[simp]
theorem nat.add_def {a b : } :
a.add b = a + b
@[simp]
theorem nat.mul_def {a b : } :
a.mul b = a * b
theorem nat.exists_eq_add_of_le {m n : } :
m n(∃ (k : ), n = m + k)
theorem nat.exists_eq_add_of_lt {m n : } :
m < n(∃ (k : ), n = m + k + 1)
theorem nat.add_pos_left {m : } (h : 0 < m) (n : ) :
0 < m + n
theorem nat.add_pos_right (m : ) {n : } (h : 0 < n) :
0 < m + n
theorem nat.add_pos_iff_pos_or_pos (m n : ) :
0 < m + n 0 < m 0 < n
theorem nat.add_eq_one_iff {a b : } :
a + b = 1 a = 0 b = 1 a = 1 b = 0
theorem nat.le_add_one_iff {i j : } :
i j + 1 i j i = j + 1
theorem nat.le_and_le_add_one_iff {x a : } :
a x x a + 1 x = a x = a + 1
theorem nat.add_succ_lt_add {a b c d : } (hab : a < b) (hcd : c < d) :
a + c + 1 < b + d

### `pred`#

@[simp]
theorem nat.add_succ_sub_one (n m : ) :
n + m.succ - 1 = n + m
@[simp]
theorem nat.succ_add_sub_one (n m : ) :
n.succ + m - 1 = n + m
theorem nat.pred_eq_sub_one (n : ) :
n.pred = n - 1
theorem nat.pred_eq_of_eq_succ {m n : } (H : m = n.succ) :
m.pred = n
@[simp]
theorem nat.pred_eq_succ_iff {n m : } :
n.pred = m.succ n = m + 2
theorem nat.pred_sub (n m : ) :
n.pred - m = (n - m).pred
theorem nat.le_pred_of_lt {n m : } (h : m < n) :
m n - 1
theorem nat.le_of_pred_lt {m n : } :
m.pred < nm n
@[simp]
theorem nat.pred_one_add (n : ) :
(1 + n).pred = n

This ensures that `simp` succeeds on `pred (n + 1) = n`.

theorem nat.pred_le_iff {n m : } :
n.pred m n m.succ

### `sub`#

Most lemmas come from the `has_ordered_sub` instance on `ℕ`.

@[protected, instance]
Equations
theorem nat.lt_pred_iff {n m : } :
n < m.pred n.succ < m
theorem nat.lt_of_lt_pred {a b : } (h : a < b - 1) :
a < b
theorem nat.le_or_le_of_add_eq_add_pred {a b c d : } (h : c + d = a + b - 1) :
a c b d
theorem nat.sub_succ' (a b : ) :
a - b.succ = a - b - 1

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

### `mul`#

theorem nat.succ_mul_pos {n : } (m : ) (hn : 0 < n) :
0 < m.succ * n
theorem nat.mul_self_le_mul_self {n m : } (h : n m) :
n * n m * m
theorem nat.mul_self_lt_mul_self {n m : } :
n < mn * n < m * m
theorem nat.mul_self_le_mul_self_iff {n m : } :
n m n * n m * m
theorem nat.mul_self_lt_mul_self_iff {n m : } :
n < m n * n < m * m
theorem nat.le_mul_self (n : ) :
n n * n
theorem nat.le_mul_of_pos_left {m n : } (h : 0 < n) :
m n * m
theorem nat.le_mul_of_pos_right {m n : } (h : 0 < n) :
m m * n
theorem nat.two_mul_ne_two_mul_add_one {n m : } :
2 * n 2 * m + 1
theorem nat.mul_eq_one_iff {a b : } :
a * b = 1 a = 1 b = 1
@[protected]
theorem nat.mul_left_inj {a b c : } (ha : 0 < a) :
b * a = c * a b = c
@[protected]
theorem nat.mul_right_inj {a b c : } (ha : 0 < a) :
a * b = a * c b = c
theorem nat.mul_left_injective {a : } (ha : 0 < a) :
function.injective (λ (x : ), x * a)
theorem nat.mul_right_injective {a : } (ha : 0 < a) :
function.injective (λ (x : ), a * x)
theorem nat.mul_ne_mul_left {a b c : } (ha : 0 < a) :
b * a c * a b c
theorem nat.mul_ne_mul_right {a b c : } (ha : 0 < a) :
a * b a * c b c
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.lt_succ_iff_lt_or_eq {n i : } :
n < i.succ n < i n = i
theorem nat.mul_self_inj {n m : } :
n * n = m * m n = m
theorem nat.le_add_pred_of_pos (n : ) {i : } (hi : i 0) :
n i + (n - 1)

### 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} (h0 : C 0) (h : Π (n : ), C nC (n + 1)) :
nat.rec h0 h 0 = h0
@[simp]
theorem nat.rec_add_one {C : Sort u} (h0 : C 0) (h : Π (n : ), C nC (n + 1)) (n : ) :
nat.rec h0 h (n + 1) = h n (nat.rec h0 h n)
def nat.le_rec_on {C : Sort u} {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 `le_rec_on'`.

Equations
• next x = _.by_cases (λ (h : n m), next next x)) (λ (h : n = m + 1), h.rec_on x)
• next x = _.rec_on x
theorem nat.le_rec_on_self {C : Sort u} {n : } {h : n n} {next : Π {k : }, C kC (k + 1)} (x : C n) :
next x = x
theorem nat.le_rec_on_succ {C : Sort u} {n m : } (h1 : n m) {h2 : n m + 1} {next : Π {k : }, C kC (k + 1)} (x : C n) :
next x = next next x)
theorem nat.le_rec_on_succ' {C : Sort u} {n : } {h : n n + 1} {next : Π {k : }, C kC (k + 1)} (x : C n) :
next x = next x
theorem nat.le_rec_on_trans {C : Sort u} {n m k : } (hnm : n m) (hmk : m k) {next : Π {k : }, C kC (k + 1)} (x : C n) :
next x = next (nat.le_rec_on hnm next x)
theorem nat.le_rec_on_succ_left {C : Sort u} {n m : } (h1 : n m) (h2 : n + 1 m) {next : Π ⦃k : ⦄, C kC (k + 1)} (x : C n) :
next (next x) = next x
theorem nat.le_rec_on_injective {C : Sort u} {n m : } (hnm : n m) (next : Π (n : ), C nC (n + 1)) (Hnext : ∀ (n : ), function.injective (next n)) :
theorem nat.le_rec_on_surjective {C : Sort u} {n m : } (hnm : n m) (next : Π (n : ), C nC (n + 1)) (Hnext : ∀ (n : ), function.surjective (next n)) :
@[protected]
def nat.strong_rec' {p : Sort u} (H : Π (n : ), (Π (m : ), m < np m)p n) (n : ) :
p n

Recursion principle based on `<`.

Equations
• = H n (λ (m : ) (hm : m < n), m)
def nat.strong_rec_on' {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
theorem nat.strong_rec_on_beta' {P : Sort u_1} {h : Π (n : ), (Π (m : ), m < nP m)P n} {n : } :
= h n (λ (m : ) (hmn : m < n), m.strong_rec_on' h)
theorem nat.le_induction {P : → Prop} {m : } (h0 : P m) (h1 : ∀ (n : ), m nP nP (n + 1)) (n : ) :
m nP n

Induction principle starting at a non-zero number. For maps to a `Sort*` see `le_rec_on`.

def nat.decreasing_induction {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {m 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 a version assuming only the assumption for `k < n`, see `decreasing_induction'`.

Equations
• hP = (λ (k : ) (ih : P kP m) (hsk : P (k + 1)), ih (h k hsk)) (λ (h : P m), h) hP
@[simp]
theorem nat.decreasing_induction_self {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {n : } (nn : n n) (hP : P n) :
hP = hP
theorem nat.decreasing_induction_succ {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {m n : } (mn : m n) (msn : m n + 1) (hP : P (n + 1)) :
hP = (h n hP)
@[simp]
theorem nat.decreasing_induction_succ' {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {m : } (msm : m m + 1) (hP : P (m + 1)) :
hP = h m hP
theorem nat.decreasing_induction_trans {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {m n k : } (mn : m n) (nk : n k) (hP : P k) :
hP = hP)
theorem nat.decreasing_induction_succ_left {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {m n : } (smn : m + 1 n) (mn : m n) (hP : P n) :
hP = h m smn hP)
def nat.even_odd_rec (n : ) (P : Sort u_1) (h0 : P 0) (h_even : Π (i : ), P iP (2 * i)) (h_odd : Π (i : ), P iP (2 * i + 1)) :
P n

Recursion principle on even and odd numbers: if we have `P 0`, and for all `i : ℕ` we can extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`. This is nothing more than a wrapper around `nat.binary_rec`, to avoid having to switch to dealing with `bit0` and `bit1`.

Equations
@[simp]
theorem nat.even_odd_rec_zero (P : Sort u_1) (h0 : P 0) (h_even : Π (i : ), P iP (2 * i)) (h_odd : Π (i : ), P iP (2 * i + 1)) :
0.even_odd_rec P h0 h_even h_odd = h0
@[simp]
theorem nat.even_odd_rec_even (n : ) (P : Sort u_1) (h0 : P 0) (h_even : Π (i : ), P iP (2 * i)) (h_odd : Π (i : ), P iP (2 * i + 1)) (H : h_even 0 h0 = h0) :
(2 * n).even_odd_rec P h0 h_even h_odd = h_even n (n.even_odd_rec P h0 h_even h_odd)
@[simp]
theorem nat.even_odd_rec_odd (n : ) (P : Sort u_1) (h0 : P 0) (h_even : Π (i : ), P iP (2 * i)) (h_odd : Π (i : ), P iP (2 * i + 1)) (H : h_even 0 h0 = h0) :
(2 * n + 1).even_odd_rec P h0 h_even h_odd = h_odd n (n.even_odd_rec P h0 h_even h_odd)
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.

def nat.strong_sub_recursion {P : Sort u_1} (H : Π (a b : ), (Π (x y : ), x < ay < bP x y)P a b) (n m : ) :
P n m

Given `P : ℕ → ℕ → Sort*`, if for all `a b : ℕ` we can extend `P` from the rectangle strictly below `(a,b)` to `P a b`, 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 n m (λ (x y : ) (hx : x < n) (hy : y < m), y)
def nat.pincer_recursion {P : Sort u_1} (Ha0 : Π (a : ), P a 0) (H0b : Π (b : ), P 0 b) (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 i 0` and `P 0 i` for all `i : ℕ`, and for any `x y : ℕ` we can extend `P` from `(x,y+1)` and `(x+1,y)` to `(x+1,y+1)` 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
def nat.le_rec_on' {C : Sort u_1} {n 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`.

Equations
• next x = _.by_cases (λ (h : n m), next h next x)) (λ (h : n = m + 1), h.rec_on x)
• next x = _.rec_on x
def nat.decreasing_induction' {P : Sort u_1} {m n : } (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 `decreasing_induction`.

Equations
• hP = (λ (n : ) (mn : m n) (ih : (Π (k : ), k < nm kP (k + 1)P k)P nP m) (h : Π (k : ), k < n + 1m kP (k + 1)P k) (hP : P (n + 1)), ih (λ (k : ) (hk : k < n), h k _) (h n _ mn hP)) (λ (h : Π (k : ), k < mm kP (k + 1)P k) (hP : P m), hP) h hP
theorem nat.set_induction_bounded {b : } {S : set } (hb : b S) (h_ind : ∀ (k : ), k Sk + 1 S) {n : } (hbn : b n) :
n S

A subset of `ℕ` containing `b : ℕ` and closed under `nat.succ` contains every `n ≥ b`.

theorem nat.set_induction {S : set } (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 `ℕ`.

theorem nat.set_eq_univ {S : set } :
0 S ∀ (k : ), k Sk + 1 S

### `div`#

@[protected]
theorem nat.div_le_of_le_mul' {m n k : } (h : m k * n) :
m / k n
@[protected]
theorem nat.div_le_self' (m n : ) :
m / n m
theorem nat.div_lt_self' (n b : ) :
(n + 1) / (b + 2) < n + 1

A version of `nat.div_lt_self` using successors, rather than additional hypotheses.

theorem nat.le_div_iff_mul_le' {x y k : } (k0 : 0 < k) :
x y / k x * k y
theorem nat.div_lt_iff_lt_mul' {x y k : } (k0 : 0 < k) :
x / k < y x < y * k
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
@[protected]
theorem nat.div_le_div_right {n m : } (h : n m) {k : } :
n / k m / k
theorem nat.lt_of_div_lt_div {m n k : } :
m / k < n / km < n
@[protected]
theorem nat.div_pos {a b : } (hba : b a) (hb : 0 < b) :
0 < a / b
@[protected]
theorem nat.div_lt_of_lt_mul {m n k : } (h : m < n * k) :
m / n < k
theorem nat.lt_mul_of_div_lt {a b c : } (h : a / c < b) (w : 0 < c) :
a < b * c
@[protected]
theorem nat.div_eq_zero_iff {a b : } (hb : 0 < b) :
a / b = 0 a < b
@[protected]
theorem nat.div_eq_zero {a b : } (hb : a < b) :
a / b = 0
theorem nat.eq_zero_of_le_div {a b : } (hb : 2 b) (h : a a / b) :
a = 0
theorem nat.mul_div_le_mul_div_assoc (a b c : ) :
a * (b / c) a * b / c
theorem nat.div_mul_div_le_div (a b c : ) :
a / c * b / a b / c
theorem nat.eq_zero_of_le_half {a : } (h : a a / 2) :
a = 0
@[protected]
theorem nat.eq_mul_of_div_eq_right {a b c : } (H1 : b a) (H2 : a / b = c) :
a = b * c
@[protected]
theorem nat.div_eq_iff_eq_mul_right {a b c : } (H : 0 < b) (H' : b a) :
a / b = c a = b * c
@[protected]
theorem nat.div_eq_iff_eq_mul_left {a b c : } (H : 0 < b) (H' : b a) :
a / b = c a = c * b
@[protected]
theorem nat.eq_mul_of_div_eq_left {a b c : } (H1 : b a) (H2 : a / b = c) :
a = c * b
@[protected]
theorem nat.lt_div_iff_mul_lt {n d : } (hnd : d n) (a : ) :
a < n / d d * a < n
@[protected]
theorem nat.mul_div_cancel_left' {a b : } (Hd : a b) :
a * (b / a) = b
@[protected]
theorem nat.mul_div_mul_left (a b : ) {c : } (hc : 0 < c) :
c * a / (c * b) = a / b

Alias of `nat.mul_div_mul`

@[protected]
theorem nat.mul_div_mul_right (a b : ) {c : } (hc : 0 < c) :
a * c / (b * c) = a / b
theorem nat.lt_div_mul_add {a b : } (hb : 0 < b) :
a < a / b * b + b
theorem nat.div_eq_iff_eq_of_dvd_dvd {n x y : } (hn : n 0) (hx : x n) (hy : y n) :
n / x = n / y x = y
theorem nat.mul_div_mul_comm_of_dvd_dvd {a b c d : } (hac : c a) (hbd : d b) :
a * b / (c * d) = a / c * (b / d)
@[protected, simp]
theorem nat.div_left_inj {a b d : } (hda : d a) (hdb : d b) :
a / d = b / d a = b

### `mod`, `dvd`#

theorem nat.mod_eq_iff_lt {a b : } (h : b 0) :
a % b = a a < b
@[simp]
theorem nat.mod_succ_eq_iff_lt {a b : } :
a % b.succ = a a < b.succ
theorem nat.div_add_mod (m k : ) :
k * (m / k) + m % k = m
theorem nat.mod_add_div' (m k : ) :
m % k + m / k * k = m
theorem nat.div_add_mod' (m k : ) :
m / k * k + m % k = m
@[protected]
theorem nat.div_mod_unique {n k m d : } (h : 0 < k) :
n / k = d n % k = m m + k * d = n m < k
theorem nat.two_mul_odd_div_two {n : } (hn : n % 2 = 1) :
2 * (n / 2) = n - 1
theorem nat.div_dvd_of_dvd {a b : } (h : b a) :
a / b a
@[protected]
theorem nat.div_div_self {a b : } :
b a0 < aa / (a / b) = b
theorem nat.mod_mul_right_div_self (a b c : ) :
a % (b * c) / b = a / b % c
theorem nat.mod_mul_left_div_self (a b c : ) :
a % (c * b) / b = a / b % c
@[protected, simp]
theorem nat.dvd_one {n : } :
n 1 n = 1
@[protected]
theorem nat.dvd_add_left {k m n : } (h : k n) :
k m + n k m
@[protected]
theorem nat.dvd_add_right {k m n : } (h : k m) :
k m + n k n
@[protected, simp]
theorem nat.not_two_dvd_bit1 (n : ) :
@[protected, 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`.

@[protected, 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' {k m n : } (h₁ : k m) (h₂ : k n) :
k m - n
theorem nat.not_dvd_of_pos_of_lt {a b : } (h1 : 0 < b) (h2 : b < a) :
¬a b
@[protected]
theorem nat.mul_dvd_mul_iff_left {a b c : } (ha : 0 < a) :
a * b a * c b c
@[protected]
theorem nat.mul_dvd_mul_iff_right {a b c : } (hc : 0 < c) :
a * c b * c a b
theorem nat.succ_div (a b : ) :
(a + 1) / b = a / b + ite (b a + 1) 1 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
@[simp]
theorem nat.mod_mod_of_dvd (n : ) {m k : } (h : m k) :
n % k % m = n % m
@[simp]
theorem nat.mod_mod (a n : ) :
a % n % n = a % n
theorem nat.sub_mod_eq_zero_of_mod_eq {a b c : } (h : a % c = b % c) :
(a - b) % c = 0

If `a` and `b` are equal mod `c`, `a - b` is zero mod `c`.

@[simp]
theorem nat.one_mod (n : ) :
1 % (n + 2) = 1
theorem nat.dvd_sub_mod {n : } (k : ) :
n k - k % n
@[simp]
theorem nat.mod_add_mod (m n k : ) :
(m % n + k) % n = (m + k) % n
@[simp]
theorem nat.add_mod_mod (m n k : ) :
(m + n % k) % k = (m + n) % k
theorem nat.add_mod (a b n : ) :
(a + b) % n = (a % n + b % n) % n
theorem nat.add_mod_eq_add_mod_right {m n k : } (i : ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
theorem nat.add_mod_eq_add_mod_left {m n k : } (i : ) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
theorem nat.add_mod_eq_ite {a b n : } :
(a + b) % n = ite (n a % n + b % n) (a % n + b % n - n) (a % n + b % n)
theorem nat.mul_mod (a b n : ) :
a * b % n = a % n * (b % n) % n
theorem nat.dvd_div_of_mul_dvd {a b c : } (h : a * b c) :
b c / a
theorem nat.mul_dvd_of_dvd_div {a b c : } (hab : c b) (h : a b / c) :
c * a b
@[simp]
theorem nat.dvd_div_iff {a b c : } (hbc : c b) :
a b / c c * a b
theorem nat.div_mul_div_comm {a b c d : } (hab : b a) (hcd : d c) :
a / b * (c / d) = a * c / (b * d)
@[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_of_dvd_of_div_eq_one {a b : } (w : a b) (h : b / a = 1) :
a = b
theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : } (w : a b) (h : b / a = 0) :
b = 0
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.div_le_div_left {a b c : } (h₁ : c b) (h₂ : 0 < c) :
a / b a / c
theorem nat.div_eq_self {a b : } :
a / b = a a = 0 b = 1
theorem nat.lt_iff_le_pred {m n : } :
0 < n(m < n m n - 1)
theorem nat.div_eq_sub_mod_div {m n : } :
m / n = (m - m % n) / n
theorem nat.mul_div_le (m n : ) :
n * (m / n) m
theorem nat.lt_mul_div_succ (m : ) {n : } (n0 : 0 < n) :
m < n * (m / n + 1)
@[simp]
theorem nat.mod_div_self (m n : ) :
m % n / n = 0
theorem nat.not_dvd_of_between_consec_multiples {n a k : } (h1 : a * k < n) (h2 : n < a * (k + 1)) :
¬a n

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

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.

`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
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
theorem nat.pred_eq_self_iff {n : } :
n.pred = n n = 0

### `find`#

theorem nat.find_eq_iff {m : } {p : → Prop} (h : ∃ (n : ), p n) :
= m p m ∀ (n : ), n < m¬p n
@[simp]
theorem nat.find_lt_iff {p : → Prop} (h : ∃ (n : ), p n) (n : ) :
< n ∃ (m : ) (H : m < n), p m
@[simp]
theorem nat.find_le_iff {p : → Prop} (h : ∃ (n : ), p n) (n : ) :
n ∃ (m : ) (H : m n), p m
@[simp]
theorem nat.le_find_iff {p : → Prop} (h : ∃ (n : ), p n) (n : ) :
n ∀ (m : ), m < n¬p m
@[simp]
theorem nat.lt_find_iff {p : → Prop} (h : ∃ (n : ), p n) (n : ) :
n < ∀ (m : ), m n¬p m
@[simp]
theorem nat.find_eq_zero {p : → Prop} (h : ∃ (n : ), p n) :
= 0 p 0
@[simp]
theorem nat.find_pos {p : → Prop} (h : ∃ (n : ), p n) :
0 < ¬p 0
theorem nat.find_mono {p q : → Prop} (h : ∀ (n : ), q np n) {hp : ∃ (n : ), p n} {hq : ∃ (n : ), q n} :
theorem nat.find_le {n : } {p : → Prop} {h : ∃ (n : ), p n} (hn : p n) :
n
theorem nat.find_add {n : } {p : → Prop} {hₘ : ∃ (m : ), p (m + n)} {hₙ : ∃ (n : ), p n} (hn : n nat.find hₙ) :
nat.find hₘ + n = nat.find hₙ
theorem nat.find_comp_succ {p : → Prop} (h₁ : ∃ (n : ), p n) (h₂ : ∃ (n : ), p (n + 1)) (h0 : ¬p 0) :
nat.find h₁ = nat.find h₂ + 1

### `find_greatest`#

@[protected]
def nat.find_greatest (P : → Prop)  :

`find_greatest P b` is the largest `i ≤ bound` such that `P i` holds, or `0` if no such `i` exists

Equations
• (n + 1) = ite (P (n + 1)) (n + 1) n)
• = 0
@[simp]
theorem nat.find_greatest_zero {P : → Prop}  :
= 0
theorem nat.find_greatest_succ {P : → Prop} (n : ) :
(n + 1) = ite (P (n + 1)) (n + 1) n)
@[simp]
theorem nat.find_greatest_eq {P : → Prop} {b : } :
P b = b
@[simp]
theorem nat.find_greatest_of_not {P : → Prop} {b : } (h : ¬P (b + 1)) :
(b + 1) =
theorem nat.find_greatest_eq_iff {m : } {P : → Prop} {b : } :
= m m b (m 0P m) ∀ ⦃n : ⦄, m < nn b¬P n
theorem nat.find_greatest_eq_zero_iff {P : → Prop} {b : } :
= 0 ∀ ⦃n : ⦄, 0 < nn b¬P n
theorem nat.find_greatest_spec {m : } {P : → Prop} {b : } (hmb : m b) (hm : P m) :
P b)
theorem nat.find_greatest_le {P : → Prop} (n : ) :
n
theorem nat.le_find_greatest {m : } {P : → Prop} {b : } (hmb : m b) (hm : P m) :
m
theorem nat.find_greatest_mono_right (P : → Prop)  :
theorem nat.find_greatest_mono_left {P Q : → Prop} (hPQ : P Q) :
theorem nat.find_greatest_mono {P Q : → Prop} {a b : } (hPQ : P Q) (hab : a b) :
theorem nat.find_greatest_is_greatest {k : } {P : → Prop} {b : } (hk : < k) (hkb : k b) :
¬P k
theorem nat.find_greatest_of_ne_zero {m : } {P : → Prop} {b : } (h : = m) (h0 : m 0) :
P m

### `bodd_div2` and `bodd`#

@[simp]
theorem nat.bodd_div2_eq (n : ) :
n.bodd_div2 = (n.bodd, n.div2)
@[simp]
theorem nat.bodd_bit0 (n : ) :
@[simp]
theorem nat.bodd_bit1 (n : ) :
@[simp]
theorem nat.div2_bit0 (n : ) :
(bit0 n).div2 = n
@[simp]
theorem nat.div2_bit1 (n : ) :
(bit1 n).div2 = n

### `bit0` and `bit1`#

@[simp]
theorem nat.bit0_eq_bit0 {m n : } :
bit0 m = bit0 n m = n
@[simp]
theorem nat.bit1_eq_bit1 {m n : } :
bit1 m = bit1 n m = n
@[simp]
theorem nat.bit1_eq_one {n : } :
bit1 n = 1 n = 0
@[simp]
theorem nat.one_eq_bit1 {n : } :
1 = bit1 n n = 0
theorem nat.bit_add (b : bool) (n m : ) :
(n + m) = + m
theorem nat.bit_add' (b : bool) (n m : ) :
(n + m) = n +
@[protected]
theorem nat.bit0_le {n m : } (h : n m) :
@[protected]
theorem nat.bit1_le {n m : } (h : n m) :
theorem nat.bit_le (b : bool) {n m : } :
n m n m
theorem nat.bit_ne_zero (b : bool) {n : } (h : n 0) :
n 0
theorem nat.bit0_le_bit (b : bool) {m n : } :
m nbit0 m n
theorem nat.bit_le_bit1 (b : bool) {m n : } :
m n m bit1 n
theorem nat.bit_lt_bit0 (b : bool) {n m : } :
n < m n < bit0 m
theorem nat.bit_lt_bit (a b : bool) {n m : } (h : n < m) :
n < m
@[simp]
theorem nat.bit0_le_bit1_iff {n k : } :
bit0 k bit1 n k n
@[simp]
theorem nat.bit0_lt_bit1_iff {n k : } :
bit0 k < bit1 n k n
@[simp]
theorem nat.bit1_le_bit0_iff {n k : } :
bit1 k bit0 n k < n
@[simp]
theorem nat.bit1_lt_bit0_iff {n k : } :
bit1 k < bit0 n k < n
@[simp]
theorem nat.one_le_bit0_iff {n : } :
1 bit0 n 0 < n
@[simp]
theorem nat.one_lt_bit0_iff {n : } :
1 < bit0 n 1 n
@[simp]
theorem nat.bit_le_bit_iff {n k : } {b : bool} :
k n k n
@[simp]
theorem nat.bit_lt_bit_iff {n k : } {b : bool} :
k < n k < n
@[simp]
theorem nat.bit_le_bit1_iff {n k : } {b : bool} :
k bit1 n k n
@[simp]
theorem nat.bit0_mod_two {n : } :
bit0 n % 2 = 0
@[simp]
theorem nat.bit1_mod_two {n : } :
bit1 n % 2 = 1
theorem nat.pos_of_bit0_pos {n : } (h : 0 < bit0 n) :
0 < n
@[simp]
theorem nat.bit_cases_on_bit {C : Sort u} (H : Π (b : bool) (n : ), C (nat.bit b n)) (b : bool) (n : ) :
(nat.bit b n).bit_cases_on H = H b n
@[simp]
theorem nat.bit_cases_on_bit0 {C : Sort u} (H : Π (b : bool) (n : ), C (nat.bit b n)) (n : ) :
@[simp]
theorem nat.bit_cases_on_bit1 {C : Sort u} (H : Π (b : bool) (n : ), C (nat.bit b n)) (n : ) :
theorem nat.bit_cases_on_injective {C : Sort u} :
function.injective (λ (H : Π (b : bool) (n : ), C (nat.bit b n)) (n : ), n.bit_cases_on H)
@[simp]
theorem nat.bit_cases_on_inj {C : Sort u} (H₁ H₂ : Π (b : bool) (n : ), C (nat.bit b n)) :
((λ (n : ), n.bit_cases_on H₁) = λ (n : ), n.bit_cases_on H₂) H₁ = H₂

### decidability of predicates #

@[protected, instance]
def nat.decidable_ball_lt (n : ) (P : Π (k : ), k < n → Prop) [H : Π (n_1 : ) (h : n_1 < n), decidable (P n_1 h)] :
decidable (∀ (n_1 : ) (h : n_1 < n), P n_1 h)
Equations
• = nat.rec (λ (P : Π (k : ), k < 0 → Prop) (H : Π (n : ) (h : n < 0), decidable (P n h)), (λ (n : ) (IH : Π (P : Π (k : ), k < n → Prop) [H : Π (n_1 : ) (h : n_1 < n), decidable (P n_1 h)], decidable (∀ (n_1 : ) (h : n_1 < n), P n_1 h)) (P : Π (k : ), k < n.succ → Prop) (H : Π (n_1 : ) (h : n_1 < n.succ), decidable (P n_1 h)), (IH (λ (k : ) (h : k < n), P k _)).cases_on (λ (h : ¬∀ (n_1 : ) (h : n_1 < n), (λ (k : ) (h : k < n), P k _) n_1 h), (λ (h : ∀ (n_1 : ) (h : n_1 < n), (λ (k : ) (h : k < n), P k _) n_1 h), dite (P n _) (λ (p : P n _), (λ (p : ¬P n _), n P
@[protected, instance]
def nat.decidable_forall_fin {n : } (P : fin n → Prop) [H : decidable_pred P] :
decidable (∀ (i : fin n), P i)
Equations
@[protected, instance]
def nat.decidable_ball_le (n : ) (P : Π (k : ), k n → Prop) [H : Π (n_1 : ) (h : n_1 n), decidable (P n_1 h)] :
decidable (∀ (n_1 : ) (h : n_1 n), P n_1 h)
Equations
@[protected, instance]
def nat.decidable_lo_hi (lo hi : ) (P : → Prop) [H : decidable_pred P] :
decidable (∀ (x : ), lo xx < hiP x)
Equations
@[protected, instance]
def nat.decidable_lo_hi_le (lo hi : ) (P : → Prop) [H : decidable_pred P] :
decidable (∀ (x : ), lo xx hiP x)
Equations
@[protected, instance]
def nat.decidable_exists_lt {P : → Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ), ∃ (m : ), m < n P m)
Equations
@[protected, instance]
def nat.decidable_exists_le {P : → Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ), ∃ (m : ), m n P m)
Equations