mathlib documentation

core / init.data.nat.lemmas

theorem nat.add_comm (n m : ) :
n + m = m + n
theorem nat.add_assoc (n m k : ) :
n + m + k = n + (m + k)
theorem nat.add_left_comm (n m k : ) :
n + (m + k) = m + (n + k)
theorem nat.add_left_cancel {n m k : } :
n + m = n + km = k
theorem nat.add_right_cancel {n m k : } (h : n + m = k + m) :
n = k
@[simp]
theorem nat.succ_ne_zero (n : ) :
n.succ 0
@[simp]
theorem nat.succ_ne_self (n : ) :
n.succ n
@[simp]
theorem nat.one_ne_zero  :
1 0
@[simp]
theorem nat.zero_ne_one  :
0 1
theorem nat.eq_zero_of_add_eq_zero_right {n m : } :
n + m = 0n = 0
theorem nat.eq_zero_of_add_eq_zero_left {n m : } (h : n + m = 0) :
m = 0
@[simp]
theorem nat.pred_zero  :
0.pred = 0
@[simp]
theorem nat.pred_succ (n : ) :
n.succ.pred = n
theorem nat.mul_zero (n : ) :
n * 0 = 0
theorem nat.mul_succ (n m : ) :
n * m.succ = n * m + n
theorem nat.zero_mul (n : ) :
0 * n = 0
theorem nat.succ_mul (n m : ) :
(n.succ) * m = n * m + m
theorem nat.right_distrib (n m k : ) :
(n + m) * k = n * k + m * k
theorem nat.left_distrib (n m k : ) :
n * (m + k) = n * m + n * k
theorem nat.mul_comm (n m : ) :
n * m = m * n
theorem nat.mul_assoc (n m k : ) :
(n * m) * k = n * m * k
theorem nat.mul_one (n : ) :
n * 1 = n
theorem nat.one_mul (n : ) :
1 * n = n
theorem nat.le_of_eq {n m : } (p : n = m) :
n m
theorem nat.le_succ_of_le {n m : } (h : n m) :
n m.succ
theorem nat.le_of_succ_le {n m : } (h : n.succ m) :
n m
theorem nat.le_of_lt {n m : } (h : n < m) :
n m
theorem nat.lt.step {n m : } :
n < mn < m.succ
theorem nat.eq_zero_or_pos (n : ) :
n = 0 0 < n
theorem nat.pos_of_ne_zero {n : } :
n 00 < n
theorem nat.lt_trans {n m k : } (h₁ : n < m) :
m < kn < k
theorem nat.lt_of_le_of_lt {n m k : } (h₁ : n m) :
m < kn < k
theorem nat.lt.base (n : ) :
n < n.succ
theorem nat.lt_succ_self (n : ) :
n < n.succ
theorem nat.le_antisymm {n m : } (h₁ : n m) :
m nn = m
theorem nat.lt_or_ge (a b : ) :
a < b b a
theorem nat.le_total {m n : } :
m n n m
theorem nat.lt_of_le_and_ne {m n : } (h1 : m n) :
m nm < n
theorem nat.lt_iff_le_not_le {m n : } :
m < n m n ¬n m
theorem nat.eq_zero_of_le_zero {n : } (h : n 0) :
n = 0
theorem nat.succ_lt_succ {a b : } :
a < ba.succ < b.succ
theorem nat.lt_of_succ_lt {a b : } :
a.succ < ba < b
theorem nat.lt_of_succ_lt_succ {a b : } :
a.succ < b.succa < b
theorem nat.pred_lt_pred {n m : } :
n 0n < mn.pred < m.pred
theorem nat.lt_of_succ_le {a b : } (h : a.succ b) :
a < b
theorem nat.succ_le_of_lt {a b : } (h : a < b) :
a.succ b
theorem nat.le_add_right (n k : ) :
n n + k
theorem nat.le_add_left (n m : ) :
n m + n
theorem nat.le.dest {n m : } :
n m(∃ (k : ), n + k = m)
theorem nat.le.intro {n m k : } (h : n + k = m) :
n m
theorem nat.add_le_add_left {n m : } (h : n m) (k : ) :
k + n k + m
theorem nat.add_le_add_right {n m : } (h : n m) (k : ) :
n + k m + k
theorem nat.le_of_add_le_add_left {k n m : } (h : k + n k + m) :
n m
theorem nat.le_of_add_le_add_right {k n m : } :
n + k m + kn m
theorem nat.add_le_add_iff_le_right (k n m : ) :
n + k m + k n m
theorem nat.lt_of_add_lt_add_left {k n m : } (h : k + n < k + m) :
n < m
theorem nat.lt_of_add_lt_add_right {a b c : } (h : a + b < c + b) :
a < c
theorem nat.add_lt_add_left {n m : } (h : n < m) (k : ) :
k + n < k + m
theorem nat.add_lt_add_right {n m : } (h : n < m) (k : ) :
n + k < m + k
theorem nat.lt_add_of_pos_right {n k : } (h : 0 < k) :
n < n + k
theorem nat.lt_add_of_pos_left {n k : } (h : 0 < k) :
n < k + n
theorem nat.add_lt_add {a b c d : } (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem nat.add_le_add {a b c d : } (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem nat.zero_lt_one  :
0 < 1
theorem nat.mul_le_mul_left {n m : } (k : ) (h : n m) :
k * n k * m
theorem nat.mul_le_mul_right {n m : } (k : ) (h : n m) :
n * k m * k
theorem nat.mul_lt_mul_of_pos_left {n m k : } (h : n < m) (hk : 0 < k) :
k * n < k * m
theorem nat.mul_lt_mul_of_pos_right {n m k : } (h : n < m) (hk : 0 < k) :
n * k < m * k
theorem nat.le_of_mul_le_mul_left {a b c : } (h : c * a c * b) (hc : 0 < c) :
a b
theorem nat.le_of_lt_succ {m n : } :
m < n.succm n
theorem nat.eq_of_mul_eq_mul_left {m k n : } (Hn : 0 < n) (H : n * m = n * k) :
m = k
@[simp]
theorem nat.zero_sub (a : ) :
0 - a = 0
theorem nat.sub_lt_succ (a b : ) :
a - b < a.succ
theorem nat.sub_le_sub_right {n m : } (h : n m) (k : ) :
n - k m - k
theorem nat.bit1_eq_succ_bit0 (n : ) :
bit1 n = (bit0 n).succ
theorem nat.bit1_succ_eq (n : ) :
theorem nat.bit1_ne_one {n : } :
n 0bit1 n 1
@[simp]
theorem nat.bit0_ne_one (n : ) :
bit0 n 1
theorem nat.add_self_ne_one (n : ) :
n + n 1
@[simp]
theorem nat.bit1_ne_bit0 (n m : ) :
@[simp]
theorem nat.bit0_ne_bit1 (n m : ) :
theorem nat.bit0_inj {n m : } :
bit0 n = bit0 mn = m
theorem nat.bit1_inj {n m : } :
bit1 n = bit1 mn = m
theorem nat.bit0_ne {n m : } :
n mbit0 n bit0 m
theorem nat.bit1_ne {n m : } :
n mbit1 n bit1 m
theorem nat.zero_ne_bit0 {n : } :
n 00 bit0 n
@[simp]
theorem nat.zero_ne_bit1 (n : ) :
0 bit1 n
@[simp]
theorem nat.one_ne_bit0 (n : ) :
1 bit0 n
theorem nat.one_ne_bit1 {n : } :
n 01 bit1 n
theorem nat.one_lt_bit1 {n : } :
n 01 < bit1 n
theorem nat.one_lt_bit0 {n : } :
n 01 < bit0 n
theorem nat.bit0_lt {n m : } (h : n < m) :
bit0 n < bit0 m
theorem nat.bit1_lt {n m : } (h : n < m) :
bit1 n < bit1 m
theorem nat.bit0_lt_bit1 {n m : } (h : n m) :
bit0 n < bit1 m
theorem nat.bit1_lt_bit0 {n m : } :
n < mbit1 n < bit0 m
theorem nat.one_le_bit1 (n : ) :
1 bit1 n
theorem nat.one_le_bit0 (n : ) :
n 01 bit0 n
@[simp]
theorem nat.sub_zero (n : ) :
n - 0 = n
theorem nat.sub_succ (n m : ) :
n - m.succ = (n - m).pred
theorem nat.succ_sub_succ (n m : ) :
n.succ - m.succ = n - m
@[simp]
theorem nat.sub_self (n : ) :
n - n = 0
theorem nat.add_sub_add_right (n k m : ) :
n + k - (m + k) = n - m
theorem nat.add_sub_add_left (k n m : ) :
k + n - (k + m) = n - m
@[simp]
theorem nat.add_sub_cancel (n m : ) :
n + m - m = n
@[simp]
theorem nat.add_sub_cancel_left (n m : ) :
n + m - n = m
theorem nat.sub_sub (n m k : ) :
n - m - k = n - (m + k)
theorem nat.le_of_le_of_sub_le_sub_right {n m k : } (h₀ : k m) (h₁ : n - k m - k) :
n m
theorem nat.sub_le_sub_right_iff (n m k : ) (h : k m) :
n - k m - k n m
theorem nat.sub_self_add (n m : ) :
n - (n + m) = 0
theorem nat.add_le_to_le_sub (x : ) {y k : } (h : k y) :
x + k y x y - k
theorem nat.sub_lt_of_pos_le (a b : ) (h₀ : 0 < a) (h₁ : a b) :
b - a < b
theorem nat.sub_one (n : ) :
n - 1 = n.pred
theorem nat.succ_sub_one (n : ) :
n.succ - 1 = n
theorem nat.succ_pred_eq_of_pos {n : } :
0 < nn.pred.succ = n
theorem nat.sub_eq_zero_of_le {n m : } (h : n m) :
n - m = 0
theorem nat.le_of_sub_eq_zero {n m : } :
n - m = 0n m
theorem nat.sub_eq_zero_iff_le {n m : } :
n - m = 0 n m
theorem nat.add_sub_of_le {n m : } (h : n m) :
n + (m - n) = m
theorem nat.sub_add_cancel {n m : } (h : m n) :
n - m + m = n
theorem nat.add_sub_assoc {m k : } (h : k m) (n : ) :
n + m - k = n + (m - k)
theorem nat.sub_eq_iff_eq_add {a b c : } (ab : b a) :
a - b = c a = c + b
theorem nat.lt_of_sub_eq_succ {m n l : } (H : m - n = l.succ) :
n < m
theorem nat.zero_min (a : ) :
min 0 a = 0
theorem nat.min_zero (a : ) :
min a 0 = 0
theorem nat.min_succ_succ (x y : ) :
min x.succ y.succ = (min x y).succ
theorem nat.sub_eq_sub_min (n m : ) :
n - m = n - min n m
@[simp]
theorem nat.sub_add_min_cancel (n m : ) :
n - m + min n m = n
def nat.strong_rec_on {p : Sort u} (n : ) (h : Π (n : ), (Π (m : ), m < np m)p n) :
p n
Equations
  • n.strong_rec_on h = (λ (this : Π (n m : ), m < n → p m), this n.succ n _) (λ (n : ), nat.rec (λ (m : ) (h₁ : m < 0), absurd h₁ _) (λ (n : ) (ih : Π (m : ), m < n → p m) (m : ) (h₁ : m < n.succ), _.by_cases (λ (ᾰ : m < n), ih m ᾰ) (λ (ᾰ : m = n), eq.rec (λ (h₁ : n < n.succ), h n ih) _ h₁)) n)
theorem nat.strong_induction_on {p : → Prop} (n : ) (h : ∀ (n : ), (∀ (m : ), m < np m)p n) :
p n
theorem nat.case_strong_induction_on {p : → Prop} (a : ) (hz : p 0) (hi : ∀ (n : ), (∀ (m : ), m np m)p n.succ) :
p a
theorem nat.mod_def (x y : ) :
x % y = ite (0 < y y x) ((x - y) % y) x
@[simp]
theorem nat.mod_zero (a : ) :
a % 0 = a
theorem nat.mod_eq_of_lt {a b : } (h : a < b) :
a % b = a
@[simp]
theorem nat.zero_mod (b : ) :
0 % b = 0
theorem nat.mod_eq_sub_mod {a b : } (h : b a) :
a % b = (a - b) % b
theorem nat.mod_lt (x : ) {y : } (h : 0 < y) :
x % y < y
@[simp]
theorem nat.mod_self (n : ) :
n % n = 0
@[simp]
theorem nat.mod_one (n : ) :
n % 1 = 0
theorem nat.mod_two_eq_zero_or_one (n : ) :
n % 2 = 0 n % 2 = 1
theorem nat.div_def (x y : ) :
x / y = ite (0 < y y x) ((x - y) / y + 1) 0
theorem nat.mod_add_div (m k : ) :
m % k + k * (m / k) = m
@[simp]
theorem nat.div_one (n : ) :
n / 1 = n
@[simp]
theorem nat.div_zero (n : ) :
n / 0 = 0
@[simp]
theorem nat.zero_div (b : ) :
0 / b = 0
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_eq_sub_div {a b : } (h₁ : 0 < b) (h₂ : b a) :
a / b = (a - b) / b + 1
theorem nat.div_eq_of_lt {a b : } (h₀ : a < b) :
a / b = 0
theorem nat.le_div_iff_mul_le (x y : ) {k : } (Hk : 0 < k) :
x y / k x * k y
theorem nat.div_lt_iff_lt_mul (x y : ) {k : } (Hk : 0 < k) :
x / k < y x < y * k
def nat.iterate {α : Sort u} (op : α → α) :
α → α
Equations
theorem nat.add_one_ne_zero (n : ) :
n + 1 0
theorem nat.eq_zero_or_eq_succ_pred (n : ) :
n = 0 n = n.pred.succ
theorem nat.exists_eq_succ_of_ne_zero {n : } (H : n 0) :
∃ (k : ), n = k.succ
def nat.discriminate {B : Sort u} {n : } (H1 : n = 0 → B) (H2 : Π (m : ), n = m.succ → B) :
B
Equations
theorem nat.one_succ_zero  :
1 = 1
def nat.two_step_induction {P : Sort u} (H1 : P 0) (H2 : P 1) (H3 : Π (n : ), P nP n.succP n.succ.succ) (a : ) :
P a
Equations
def nat.sub_induction {P : Sort u} (H1 : Π (m : ), P 0 m) (H2 : Π (n : ), P n.succ 0) (H3 : Π (n m : ), P n mP n.succ m.succ) (n m : ) :
P n m
Equations
theorem nat.succ_add_eq_succ_add (n m : ) :
n.succ + m = n + m.succ
theorem nat.add_right_comm (n m k : ) :
n + m + k = n + k + m
theorem nat.eq_zero_of_add_eq_zero {n m : } (H : n + m = 0) :
n = 0 m = 0
theorem nat.eq_zero_of_mul_eq_zero {n m : } :
n * m = 0n = 0 m = 0
theorem nat.le_succ_of_pred_le {n m : } :
n.pred mn m.succ
theorem nat.le_lt_antisymm {n m : } (h₁ : n m) (h₂ : m < n) :
theorem nat.lt_le_antisymm {n m : } (h₁ : n < m) (h₂ : m n) :
theorem nat.lt_asymm {n m : } (h₁ : n < m) :
¬m < n
def nat.lt_ge_by_cases {a b : } {C : Sort u} (h₁ : a < b → C) (h₂ : b a → C) :
C
Equations
def nat.lt_by_cases {a b : } {C : Sort u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) :
C
Equations
theorem nat.lt_trichotomy (a b : ) :
a < b a = b b < a
theorem nat.eq_or_lt_of_not_lt {a b : } (hnlt : ¬a < b) :
a = b b < a
theorem nat.lt_succ_of_lt {a b : } (h : a < b) :
a < b.succ
theorem nat.one_pos  :
0 < 1
theorem nat.sub_le_sub_left {n m : } (k : ) (h : n m) :
k - m k - n
theorem nat.succ_sub_sub_succ (n m k : ) :
n.succ - m - k.succ = n - m - k
theorem nat.sub.right_comm (m n k : ) :
m - n - k = m - k - n
theorem nat.mul_pred_left (n m : ) :
(n.pred) * m = n * m - m
theorem nat.mul_pred_right (n m : ) :
n * m.pred = n * m - n
theorem nat.mul_sub_right_distrib (n m k : ) :
(n - m) * k = n * k - m * k
theorem nat.mul_sub_left_distrib (n m k : ) :
n * (m - k) = n * m - n * k
theorem nat.mul_self_sub_mul_self_eq (a b : ) :
a * a - b * b = (a + b) * (a - b)
theorem nat.succ_mul_succ_eq (a b : ) :
(a.succ) * b.succ = a * b + a + b + 1
theorem nat.succ_sub {m n : } (h : n m) :
m.succ - n = (m - n).succ
theorem nat.sub_pos_of_lt {m n : } (h : m < n) :
0 < n - m
theorem nat.sub_sub_self {n m : } (h : m n) :
n - (n - m) = m
theorem nat.sub_add_comm {n m k : } (h : k n) :
n + m - k = n - k + m
theorem nat.sub_one_sub_lt {n i : } (h : i < n) :
n - 1 - i < n
theorem nat.pred_inj {a b : } :
0 < a0 < ba.pred = b.preda = b
def nat.find_x {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) :
{n // p n ∀ (m : ), m < n¬p m}
Equations
  • nat.find_x H = _.fix (λ (m : ) (IH : Π (y : ), lbp y m(λ (k : ), (∀ (n : ), n < k¬p n){n // p n ∀ (m : ), m < n¬p m}) y) (al : ∀ (n : ), n < m¬p n), dite (p m) (λ (pm : p m), m, _⟩) (λ (pm : ¬p m), have this : ∀ (n : ), n m¬p n, from _, IH (m + 1) _ _)) 0 nat.find_x._proof_5
def nat.find {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) :

If p is a (decidable) predicate on and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then nat.find hp is the smallest natural number satisfying p. Note that nat.find is protected, meaning that you can't just write find, even if the nat namespace is open.

The API for nat.find is:

Equations
theorem nat.find_spec {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) :
p (nat.find H)
theorem nat.find_min {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) {m : } :
m < nat.find H¬p m
theorem nat.find_min' {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) {m : } (h : p m) :
theorem nat.mod_le (x y : ) :
x % y x
@[simp]
theorem nat.add_mod_right (x z : ) :
(x + z) % z = x % z
@[simp]
theorem nat.add_mod_left (x z : ) :
(x + z) % x = z % x
@[simp]
theorem nat.add_mul_mod_self_left (x y z : ) :
(x + y * z) % y = x % y
@[simp]
theorem nat.add_mul_mod_self_right (x y z : ) :
(x + y * z) % z = x % z
@[simp]
theorem nat.mul_mod_right (m n : ) :
m * n % m = 0
@[simp]
theorem nat.mul_mod_left (m n : ) :
m * n % n = 0
theorem nat.mul_mod_mul_left (z x y : ) :
z * x % z * y = z * (x % y)
theorem nat.mul_mod_mul_right (z x y : ) :
x * z % y * z = (x % y) * z
theorem nat.cond_to_bool_mod_two (x : ) [d : decidable (x % 2 = 1)] :
cond (to_bool (x % 2 = 1)) 1 0 = x % 2
theorem nat.sub_mul_mod (x k n : ) (h₁ : n * k x) :
(x - n * k) % n = x % n
theorem nat.sub_mul_div (x n p : ) (h₁ : n * p x) :
(x - n * p) / n = x / n - p
theorem nat.div_mul_le_self (m n : ) :
(m / n) * n m
@[simp]
theorem nat.add_div_right (x : ) {z : } (H : 0 < z) :
(x + z) / z = (x / z).succ
@[simp]
theorem nat.add_div_left (x : ) {z : } (H : 0 < z) :
(z + x) / z = (x / z).succ
@[simp]
theorem nat.mul_div_right (n : ) {m : } (H : 0 < m) :
m * n / m = n
@[simp]
theorem nat.mul_div_left (m : ) {n : } (H : 0 < n) :
m * n / n = m
@[simp]
theorem nat.div_self {n : } (H : 0 < n) :
n / n = 1
theorem nat.add_mul_div_left (x z : ) {y : } (H : 0 < y) :
(x + y * z) / y = x / y + z
theorem nat.add_mul_div_right (x y : ) {z : } (H : 0 < z) :
(x + y * z) / z = x / z + y
theorem nat.mul_div_cancel (m : ) {n : } (H : 0 < n) :
m * n / n = m
theorem nat.mul_div_cancel_left (m : ) {n : } (H : 0 < n) :
n * m / n = m
theorem nat.div_eq_of_eq_mul_left {m n k : } (H1 : 0 < n) (H2 : m = k * n) :
m / n = k
theorem nat.div_eq_of_eq_mul_right {m n k : } (H1 : 0 < n) (H2 : m = n * k) :
m / n = k
theorem nat.div_eq_of_lt_le {m n k : } (lo : k * n m) (hi : m < (k.succ) * n) :
m / n = k
theorem nat.mul_sub_div (x n p : ) (h₁ : x < n * p) :
(n * p - x.succ) / n = p - (x / n).succ
theorem nat.mul_pos {a b : } (ha : 0 < a) (hb : 0 < b) :
0 < a * b
theorem nat.div_div_eq_div_mul (m n k : ) :
m / n / k = m / n * k
theorem nat.mul_div_mul {m : } (n k : ) (H : 0 < m) :
m * n / m * k = n / k
theorem nat.dvd_mul_right (a b : ) :
a a * b
theorem nat.dvd_trans {a b c : } (h₁ : a b) (h₂ : b c) :
a c
theorem nat.eq_zero_of_zero_dvd {a : } (h : 0 a) :
a = 0
theorem nat.dvd_add {a b c : } (h₁ : a b) (h₂ : a c) :
a b + c
theorem nat.dvd_add_iff_right {k m n : } (h : k m) :
k n k m + n
theorem nat.dvd_add_iff_left {k m n : } (h : k n) :
k m k m + n
theorem nat.dvd_sub {k m n : } (H : n m) (h₁ : k m) (h₂ : k n) :
k m - n
theorem nat.dvd_mod_iff {k m n : } (h : k n) :
k m % n k m
theorem nat.le_of_dvd {m n : } (h : 0 < n) :
m nm n
theorem nat.dvd_antisymm {m n : } :
m nn mm = n
theorem nat.pos_of_dvd_of_pos {m n : } (H1 : m n) (H2 : 0 < n) :
0 < m
theorem nat.eq_one_of_dvd_one {n : } (H : n 1) :
n = 1
theorem nat.dvd_of_mod_eq_zero {m n : } (H : n % m = 0) :
m n
theorem nat.mod_eq_zero_of_dvd {m n : } (H : m n) :
n % m = 0
theorem nat.dvd_iff_mod_eq_zero (m n : ) :
m n n % m = 0
theorem nat.mul_div_cancel' {m n : } (H : n m) :
n * (m / n) = m
theorem nat.div_mul_cancel {m n : } (H : n m) :
(m / n) * n = m
theorem nat.mul_div_assoc (m : ) {n k : } (H : k n) :
m * n / k = m * (n / k)
theorem nat.dvd_of_mul_dvd_mul_left {m n k : } (kpos : 0 < k) (H : k * m k * n) :
m n
theorem nat.dvd_of_mul_dvd_mul_right {m n k : } (kpos : 0 < k) (H : m * k n * k) :
m n
theorem nat.mul_le_mul_of_nonneg_left {a b c : } (h₁ : a b) :
c * a c * b
theorem nat.mul_le_mul_of_nonneg_right {a b c : } (h₁ : a b) :
a * c b * c
theorem nat.mul_lt_mul {a b c d : } (hac : a < c) (hbd : b d) (pos_b : 0 < b) :
a * b < c * d
theorem nat.mul_lt_mul' {a b c d : } (h1 : a c) (h2 : b < d) (h3 : 0 < c) :
a * b < c * d
theorem nat.mul_le_mul {a b c d : } (hac : a c) (hbd : b d) :
a * b c * d
theorem nat.div_lt_self {n m : } :
0 < n1 < mn / m < n