mathlib documentation

data.nat.basic

Basic operations on the natural numbers

This file contains:

instances

@[instance]

Extra instances to short-circuit type class resolution

@[instance]

Equations
theorem nat.eq_of_mul_eq_mul_right {n m k : } :
0 < mn * m = k * mn = k

@[instance]

Equations

Inject some simple facts into the type class system. This fact should not be confused with the factorial function nat.fact!

@[instance]
def succ_pos'' (n : ) :
fact (0 < n.succ)

@[instance]
def pos_of_one_lt (n : ) [h : fact (1 < n)] :
fact (0 < n)

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} set.range f

The units of the natural numbers as a monoid and add_monoid

theorem nat.units_eq_one (u : units ) :
u = 1

theorem nat.add_units_eq_zero (u : add_units ) :
u = 0

@[simp]
theorem nat.is_unit_iff {n : } :
is_unit n n = 1

Equalities and inequalities involving zero and one

theorem nat.pos_iff_ne_zero {n : } :
0 < n n 0

theorem nat.one_lt_iff_ne_zero_and_ne_one {n : } :
1 < n n 0 n 1

theorem nat.mul_ne_zero {n m : } :
n 0m 0n * m 0

@[simp]
theorem nat.mul_eq_zero {a b : } :
a * b = 0 a = 0 b = 0

@[simp]
theorem nat.zero_eq_mul {a b : } :
0 = a * b a = 0 b = 0

theorem nat.eq_zero_of_double_le {a : } :
2 * a aa = 0

theorem nat.eq_zero_of_mul_le {a b : } :
2 bb * a aa = 0

theorem nat.le_zero_iff {i : } :
i 0 i = 0

theorem nat.zero_max {m : } :
max 0 m = m

theorem nat.one_le_of_lt {n m : } :
n < m1 m

succ

theorem nat.eq_of_lt_succ_of_not_lt {a b : } :
a < b + 1¬a < ba = b

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_le_succ_iff {m n : } :
m.succ n.succ m n

theorem nat.max_succ_succ {m n : } :
max m.succ n.succ = (max m 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 : } :
n m.succn m n = m.succ

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 : } :
0 < n0 < 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.add_succ_lt_add {a b c d : } :
a < bc < da + 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 : } :
m = n.succm.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 : } :
m < nm 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.

sub

theorem nat.le_sub_add (n m : ) :
n n - m + m

theorem nat.sub_add_eq_max (n m : ) :
n - m + m = max n m

theorem nat.add_sub_eq_max (n m : ) :
n + (m - n) = max n m

theorem nat.sub_add_min (n m : ) :
n - m + min n m = n

theorem nat.add_sub_cancel' {n m : } :
m nm + (n - m) = n

theorem nat.sub_add_sub_cancel {a b c : } :
b ac ba - b + (b - c) = a - c

theorem nat.sub_eq_of_eq_add {m n k : } :
k = m + nk - m = n

theorem nat.sub_cancel {a b c : } :
a ba cb - a = c - ab = c

theorem nat.sub_sub_sub_cancel_right {a b c : } :
c ba - c - (b - c) = a - b

theorem nat.add_sub_cancel_right (n m k : ) :
n + (m + k) - k = n + m

theorem nat.sub_add_eq_add_sub {a b c : } :
b aa - b + c = a + c - b

theorem nat.sub_min (n m : ) :
n - min n m = n - m

theorem nat.sub_sub_assoc {a b c : } :
b ac ba - (b - c) = a - b + c

theorem nat.lt_of_sub_pos {m n : } :
0 < n - mm < n

theorem nat.lt_of_sub_lt_sub_right {m n k : } :
m - k < n - km < n

theorem nat.lt_of_sub_lt_sub_left {m n k : } :
m - n < m - kk < n

theorem nat.sub_lt_self {m n : } :
0 < m0 < nm - n < m

theorem nat.le_sub_right_of_add_le {m n k : } :
m + k nm n - k

theorem nat.le_sub_left_of_add_le {m n k : } :
k + m nm n - k

theorem nat.lt_sub_right_of_add_lt {m n k : } :
m + k < nm < n - k

theorem nat.lt_sub_left_of_add_lt {m n k : } :
k + m < nm < n - k

theorem nat.add_lt_of_lt_sub_right {m n k : } :
m < n - km + k < n

theorem nat.add_lt_of_lt_sub_left {m n k : } :
m < n - kk + m < n

theorem nat.le_add_of_sub_le_right {m n k : } :
n - k mn m + k

theorem nat.le_add_of_sub_le_left {m n k : } :
n - k mn k + m

theorem nat.lt_add_of_sub_lt_right {m n k : } :
n - k < mn < m + k

theorem nat.lt_add_of_sub_lt_left {m n k : } :
n - k < mn < k + m

theorem nat.sub_le_left_of_le_add {m n k : } :
n k + mn - k m

theorem nat.sub_le_right_of_le_add {m n k : } :
n m + kn - k m

theorem nat.sub_lt_left_iff_lt_add {m n k : } :
n k(k - n < m k < n + m)

theorem nat.le_sub_left_iff_add_le {m n k : } :
m k(n k - m m + n k)

theorem nat.le_sub_right_iff_add_le {m n k : } :
n k(m k - n m + n k)

theorem nat.lt_sub_left_iff_add_lt {m n k : } :
n < k - m m + n < k

theorem nat.lt_sub_right_iff_add_lt {m n k : } :
m < k - n m + n < k

theorem nat.sub_le_left_iff_le_add {m n k : } :
m - n k m n + k

theorem nat.sub_le_right_iff_le_add {m n k : } :
m - k n m n + k

theorem nat.sub_lt_right_iff_lt_add {m n k : } :
k m(m - k < n m < n + k)

theorem nat.sub_le_sub_left_iff {m n k : } :
k m(m - n m - k k n)

theorem nat.sub_lt_sub_right_iff {m n k : } :
k m(m - k < n - k m < n)

theorem nat.sub_lt_sub_left_iff {m n k : } :
n m(m - n < m - k k < n)

theorem nat.sub_le_iff {m n k : } :
m - n k m - k n

theorem nat.sub_le_self (n m : ) :
n - m n

theorem nat.sub_lt_iff {m n k : } :
n mk m(m - n < k m - k < n)

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

theorem nat.lt_pred_iff {n m : } :
n < m.pred n.succ < m

theorem nat.lt_of_lt_pred {a b : } :
a < b - 1a < b

mul

theorem nat.mul_self_le_mul_self {n m : } :
n mn * 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 : } :
0 < nm n * m

theorem nat.le_mul_of_pos_right {m n : } :
0 < nm 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

theorem nat.mul_left_inj {a b c : } :
0 < a(b * a = c * a b = c)

theorem nat.mul_right_inj {a b c : } :
0 < a(a * b = a * c b = c)

theorem nat.mul_right_eq_self_iff {a b : } :
0 < a(a * b = a b = 1)

theorem nat.mul_left_eq_self_iff {a b : } :
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

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.

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.

Equations
theorem nat.le_rec_on_self {C : Sort u} {n : } {h : n n} {next : Π {k : }, C kC (k + 1)} (x : C n) :
nat.le_rec_on h 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) :
nat.le_rec_on h2 next x = next (nat.le_rec_on h1 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) :
nat.le_rec_on h 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) :
nat.le_rec_on _ next x = nat.le_rec_on hmk 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) :
nat.le_rec_on h2 next (next x) = nat.le_rec_on h1 next x

theorem nat.le_rec_on_injective {C : Sort u} {n m : } (hnm : n m) (next : Π (n : ), C nC (n + 1)) :
(∀ (n : ), function.injective (next n))function.injective (nat.le_rec_on hnm next)

theorem nat.le_rec_on_surjective {C : Sort u} {n m : } (hnm : n m) (next : Π (n : ), C nC (n + 1)) :
(∀ (n : ), function.surjective (next n))function.surjective (nat.le_rec_on hnm next)

def nat.strong_rec' {p : Sort u} (H : Π (n : ), (Π (m : ), m < np m)p n) (n : ) :
p n

Recursion principle based on <.

Equations
def nat.strong_rec_on' {P : Sort u_1} (n : ) :
(Π (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 : } :
n.strong_rec_on' h = 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 : } :
m nP nP 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*.

Equations
@[simp]
theorem nat.decreasing_induction_self {P : Sort u_1} (h : Π (n : ), P (n + 1)P n) {n : } (nn : n n) (hP : P n) :

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

@[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)) :
nat.decreasing_induction h msm 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) :

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

div

theorem nat.div_le_of_le_mul' {m n k : } :
m k * nm / k n

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 : } :
0 < k(x y / k x * k y)

theorem nat.div_mul_le_self' (m n : ) :
(m / n) * n m

theorem nat.div_lt_iff_lt_mul' {x y k : } :
0 < k(x / k < y x < y * k)

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

theorem nat.div_pos {a b : } :
b a0 < b0 < a / b

theorem nat.div_lt_of_lt_mul {m n k : } :
m < n * km / n < k

theorem nat.lt_mul_of_div_lt {a b c : } :
a / c < b0 < ca < b * c

theorem nat.div_eq_zero_iff {a b : } :
0 < b(a / b = 0 a < b)

theorem nat.div_eq_zero {a b : } :
a < ba / b = 0

theorem nat.eq_zero_of_le_div {a b : } :
2 ba a / ba = 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 : } :
a a / 2a = 0

theorem nat.eq_mul_of_div_eq_right {a b c : } :
b aa / b = ca = b * c

theorem nat.div_eq_iff_eq_mul_right {a b c : } :
0 < bb a(a / b = c a = b * c)

theorem nat.div_eq_iff_eq_mul_left {a b c : } :
0 < bb a(a / b = c a = c * b)

theorem nat.eq_mul_of_div_eq_left {a b c : } :
b aa / b = ca = c * b

theorem nat.mul_div_cancel_left' {a b : } :
a ba * (b / a) = b

mod, dvd

theorem nat.div_mod_unique {n k m d : } :
0 < k(n / k = d n % k = m m + k * d = n m < k)

theorem nat.two_mul_odd_div_two {n : } :
n % 2 = 12 * (n / 2) = n - 1

theorem nat.div_dvd_of_dvd {a b : } :
b aa / b a

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

@[simp]
theorem nat.dvd_one {n : } :
n 1 n = 1

theorem nat.dvd_add_left {k m n : } :
k n(k m + n k m)

theorem nat.dvd_add_right {k m n : } :
k m(k m + n k n)

@[simp]
theorem nat.not_two_dvd_bit1 (n : ) :

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

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

theorem nat.mul_dvd_mul_iff_left {a b c : } :
0 < a(a * b a * c b c)

theorem nat.mul_dvd_mul_iff_right {a b c : } :
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 : } :
b a + 1(a + 1) / b = a / b + 1

theorem nat.succ_div_of_not_dvd {a b : } :
¬b a + 1(a + 1) / b = a / b

@[simp]
theorem nat.mod_mod_of_dvd (n : ) {m k : } :
m kn % 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 : } :
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 : ) :
m % n = k % n(m + i) % n = (k + i) % n

theorem nat.add_mod_eq_add_mod_left {m n k : } (i : ) :
m % n = k % n(i + m) % n = (i + k) % 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 : } :
a * b cb c / a

theorem nat.mul_dvd_of_dvd_div {a b c : } :
c ba b / cc * a b

theorem nat.div_mul_div {a b c d : } :
b ad c(a / b) * (c / d) = a * c / b * d

@[simp]
theorem nat.div_div_div_eq_div {a b c : } :
b aa cc / (a / b) / b = c / a

theorem nat.eq_of_dvd_of_div_eq_one {a b : } :
a bb / a = 1a = b

theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : } :
a bb / a = 0b = 0

theorem nat.eq_zero_of_dvd_of_lt {a b : } :
a bb < ab = 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 : } :
c b0 < ca / b a / c

theorem nat.div_eq_self {a b : } :
a / b = a a = 0 b = 1

pow

theorem nat.pow_le_pow_of_le_left {x y : } (H : x y) (i : ) :
x ^ i y ^ i

theorem nat.pow_le_pow_of_le_right {x : } (H : x > 0) {i j : } :
i jx ^ i x ^ j

theorem nat.pow_lt_pow_of_lt_left {x y : } (H : x < y) {i : } :
0 < ix ^ i < y ^ i

theorem nat.pow_lt_pow_of_lt_right {x : } (H : x > 1) {i j : } :
i < jx ^ i < x ^ j

theorem nat.pow_lt_pow_succ {p : } (h : 1 < p) (n : ) :
p ^ n < p ^ (n + 1)

theorem nat.lt_pow_self {p : } (h : 1 < p) (n : ) :
n < p ^ n

theorem nat.lt_two_pow (n : ) :
n < 2 ^ n

theorem nat.one_le_pow (n m : ) :
0 < m1 m ^ n

theorem nat.one_le_pow' (n m : ) :
1 (m + 1) ^ n

theorem nat.one_le_two_pow (n : ) :
1 2 ^ n

theorem nat.one_lt_pow (n m : ) :
0 < n1 < m1 < m ^ n

theorem nat.one_lt_pow' (n m : ) :
1 < (m + 2) ^ (n + 1)

theorem nat.one_lt_two_pow (n : ) :
0 < n1 < 2 ^ n

theorem nat.one_lt_two_pow' (n : ) :
1 < 2 ^ (n + 1)

theorem nat.pow_right_strict_mono {x : } :
2 xstrict_mono (λ (n : ), x ^ n)

theorem nat.pow_le_iff_le_right {x m n : } :
2 x(x ^ m x ^ n m n)

theorem nat.pow_lt_iff_lt_right {x m n : } :
2 x(x ^ m < x ^ n m < n)

theorem nat.pow_right_injective {x : } :
2 xfunction.injective (λ (n : ), x ^ n)

theorem nat.pow_left_strict_mono {m : } :
1 mstrict_mono (λ (x : ), x ^ m)

theorem nat.pow_le_iff_le_left {m x y : } :
1 m(x ^ m y ^ m x y)

theorem nat.pow_lt_iff_lt_left {m x y : } :
1 m(x ^ m < y ^ m x < y)

theorem nat.pow_left_injective {m : } :
1 mfunction.injective (λ (x : ), x ^ m)

pow and mod / dvd

theorem nat.mod_pow_succ {b : } (b_pos : 0 < b) (w m : ) :
m % b ^ w.succ = b * (m / b % b ^ w) + m % b

theorem nat.pow_dvd_pow_iff_pow_le_pow {k l x : } :
0 < x(x ^ k x ^ l x ^ k x ^ l)

theorem nat.pow_dvd_pow_iff_le_right {x k l : } :
1 < x(x ^ k x ^ l k l)

If 1 < x, then x^k divides x^l if and only if k is at most l.

theorem nat.pow_dvd_pow_iff_le_right' {b k l : } :
(b + 2) ^ k (b + 2) ^ l k l

theorem nat.not_pos_pow_dvd {p k : } :
1 < p1 < k¬p ^ k p

theorem nat.pow_dvd_of_le_of_pow_dvd {p m n k : } :
m np ^ n kp ^ m k

theorem nat.dvd_of_pow_dvd {p k m : } :
1 kp ^ k mp m

theorem nat.exists_lt_and_lt_iff_not_dvd (m : ) {n : } :
0 < n((∃ (k : ), n * k < m m < n * (k + 1)) ¬n m)

m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

find

theorem nat.find_eq_iff {p : → Prop} [decidable_pred p] (h : ∃ (n : ), p n) {m : } :
nat.find h = m p m ∀ (n : ), n < m¬p n

@[simp]
theorem nat.find_eq_zero {p : → Prop} [decidable_pred p] (h : ∃ (n : ), p n) :
nat.find h = 0 p 0

@[simp]
theorem nat.find_pos {p : → Prop} [decidable_pred p] (h : ∃ (n : ), p n) :
0 < nat.find h ¬p 0

find_greatest

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

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

Equations
@[simp]
theorem nat.find_greatest_zero {P : → Prop} [decidable_pred P] :

@[simp]
theorem nat.find_greatest_eq {P : → Prop} [decidable_pred P] {b : } :
P bnat.find_greatest P b = b

@[simp]
theorem nat.find_greatest_of_not {P : → Prop} [decidable_pred P] {b : } :
¬P (b + 1)nat.find_greatest P (b + 1) = nat.find_greatest P b

theorem nat.find_greatest_eq_iff {P : → Prop} [decidable_pred P] {b m : } :
nat.find_greatest P b = m m b (m 0P m) ∀ ⦃n : ⦄, m < nn b¬P n

theorem nat.find_greatest_eq_zero_iff {P : → Prop} [decidable_pred P] {b : } :
nat.find_greatest P b = 0 ∀ ⦃n : ⦄, 0 < nn b¬P n

theorem nat.find_greatest_spec {P : → Prop} [decidable_pred P] {b : } :
(∃ (m : ), m b P m)P (nat.find_greatest P b)

theorem nat.find_greatest_le {P : → Prop} [decidable_pred P] {b : } :

theorem nat.le_find_greatest {P : → Prop} [decidable_pred P] {b m : } :
m bP mm nat.find_greatest P b

theorem nat.find_greatest_is_greatest {P : → Prop} [decidable_pred P] {b k : } :
nat.find_greatest P b < kk b¬P k

theorem nat.find_greatest_of_ne_zero {P : → Prop} [decidable_pred P] {b m : } :
nat.find_greatest P b = mm 0P 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

theorem nat.bit0_le {n m : } :
n mbit0 n bit0 m

theorem nat.bit1_le {n m : } :
n mbit1 n bit1 m

theorem nat.bit_le (b : bool) {n m : } :
n mnat.bit b n nat.bit b m

theorem nat.bit_ne_zero (b : bool) {n : } :
n 0nat.bit b n 0

theorem nat.bit0_le_bit (b : bool) {m n : } :
m nbit0 m nat.bit b n

theorem nat.bit_le_bit1 (b : bool) {m n : } :
m nnat.bit b m bit1 n

theorem nat.bit_lt_bit0 (b : bool) {n m : } :
n < mnat.bit b n < bit0 m

theorem nat.bit_lt_bit (a b : bool) {n m : } :
n < mnat.bit a n < nat.bit b 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} :
nat.bit b k nat.bit b n k n

@[simp]
theorem nat.bit_lt_bit_iff {n k : } {b : bool} :
nat.bit b k < nat.bit b n k < n

@[simp]
theorem nat.bit_le_bit1_iff {n k : } {b : bool} :
nat.bit b 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 : } :
0 < bit0 n0 < n

def nat.bit_cases {C : Sort u} (H : Π (b : bool) (n : ), C (nat.bit b n)) (n : ) :
C n

Define a function on depending on parity of the argument.

Equations

shiftl and shiftr

theorem nat.shiftl_eq_mul_pow (m n : ) :
m.shiftl n = m * 2 ^ n

theorem nat.shiftl'_tt_eq_mul_pow (m n : ) :
nat.shiftl' tt m n + 1 = (m + 1) * 2 ^ n

theorem nat.one_shiftl (n : ) :
1.shiftl n = 2 ^ n

@[simp]
theorem nat.zero_shiftl (n : ) :
0.shiftl n = 0

theorem nat.shiftr_eq_div_pow (m n : ) :
m.shiftr n = m / 2 ^ n

@[simp]
theorem nat.zero_shiftr (n : ) :
0.shiftr n = 0

theorem nat.shiftl'_ne_zero_left (b : bool) {m : } (h : m 0) (n : ) :

theorem nat.shiftl'_tt_ne_zero (m : ) {n : } :
n 0nat.shiftl' tt m n 0

size

@[simp]
theorem nat.size_zero  :
0.size = 0

@[simp]
theorem nat.size_bit {b : bool} {n : } :
nat.bit b n 0(nat.bit b n).size = n.size.succ

@[simp]
theorem nat.size_bit0 {n : } :
n 0(bit0 n).size = n.size.succ

@[simp]
theorem nat.size_bit1 (n : ) :

@[simp]
theorem nat.size_one  :
1.size = 1

@[simp]
theorem nat.size_shiftl' {b : bool} {m n : } :
nat.shiftl' b m n 0(nat.shiftl' b m n).size = m.size + n

@[simp]
theorem nat.size_shiftl {m : } (h : m 0) (n : ) :
(m.shiftl n).size = m.size + n

theorem nat.lt_size_self (n : ) :
n < 2 ^ n.size

theorem nat.size_le {m n : } :
m.size n m < 2 ^ n

theorem nat.lt_size {m n : } :
m < n.size 2 ^ m n

theorem nat.size_pos {n : } :
0 < n.size 0 < n

theorem nat.size_eq_zero {n : } :
n.size = 0 n = 0

theorem nat.size_pow {n : } :
(2 ^ n).size = n + 1

theorem nat.size_le_size {m n : } :
m nm.size n.size

decidability of predicates

@[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
@[instance]
def nat.decidable_forall_fin {n : } (P : fin n → Prop) [H : decidable_pred P] :
decidable (∀ (i : fin n), P i)

Equations
@[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
@[instance]
def nat.decidable_lo_hi (lo hi : ) (P : → Prop) [H : decidable_pred P] :
decidable (∀ (x : ), lo xx < hiP x)

Equations
@[instance]
def nat.decidable_lo_hi_le (lo hi : ) (P : → Prop) [H : decidable_pred P] :
decidable (∀ (x : ), lo xx hiP x)

Equations