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