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 : } :
n + m = k + mn = k

theorem nat.succ_ne_zero (n : ) :
n.succ 0

theorem nat.succ_ne_self (n : ) :
n.succ n

theorem nat.one_ne_zero  :
1 0

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 : } :
n + m = 0m = 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 : } :
n = mn m

theorem nat.le_succ_of_le {n m : } :
n mn m.succ

theorem nat.le_of_succ_le {n m : } :
n.succ mn m

theorem nat.le_of_lt {n m : } :
n < mn m

def nat.lt.step {n m : } :
n < mn < m.succ

theorem nat.eq_zero_or_pos (n : ) :
n = 0 n > 0

theorem nat.pos_of_ne_zero {n : } :
n 0n > 0

theorem nat.lt_trans {n m k : } :
n < mm < kn < k

theorem nat.lt_of_le_of_lt {n m k : } :
n mm < kn < k

def nat.lt.base (n : ) :
n < n.succ

theorem nat.lt_succ_self (n : ) :
n < n.succ

theorem nat.le_antisymm {n m : } :
n mm nn = m

theorem nat.lt_or_ge (a b : ) :
a < b a b

theorem nat.le_total {m n : } :
m n n m

theorem nat.lt_of_le_and_ne {m n : } :
m nm 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 : } :
n 0n = 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 : } :
a.succ ba < b

theorem nat.succ_le_of_lt {a b : } :
a < ba.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 : } :
n + k = mn 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 : } :
k + n k + mn 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 : } :
k + n < k + mn < m

theorem nat.lt_of_add_lt_add_right {a b c : } :
a + b < c + ba < 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 : } :
k > 0n < n + k

theorem nat.lt_add_of_pos_left {n k : } :
k > 0n < k + n

theorem nat.add_lt_add {a b c d : } :
a < bc < da + c < b + d

theorem nat.add_le_add {a b c d : } :
a bc da + c b + d

theorem nat.zero_lt_one  :
0 < 1

theorem nat.mul_le_mul_left {n m : } (k : ) :
n mk * n k * m

theorem nat.mul_le_mul_right {n m : } (k : ) :
n mn * k m * k

theorem nat.mul_lt_mul_of_pos_left {n m k : } :
n < mk > 0k * n < k * m

theorem nat.mul_lt_mul_of_pos_right {n m k : } :
n < mk > 0n * k < m * k

theorem nat.le_of_mul_le_mul_left {a b c : } :
c * a c * bc > 0a b

theorem nat.le_of_lt_succ {m n : } :
m < n.succm n

theorem nat.eq_of_mul_eq_mul_left {m k n : } :
n > 0n * m = n * km = 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

theorem nat.bit0_ne_one (n : ) :
bit0 n 1

theorem nat.add_self_ne_one (n : ) :
n + n 1

theorem nat.bit1_ne_bit0 (n m : ) :

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

theorem nat.zero_ne_bit1 (n : ) :
0 bit1 n

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 : } :
n < mbit0 n < bit0 m

theorem nat.bit1_lt {n m : } :
n < mbit1 n < bit1 m

theorem nat.bit0_lt_bit1 {n m : } :
n mbit0 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 : } :
k mn - k m - kn m

theorem nat.sub_le_sub_right_iff (n m k : ) :
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 : } :
k y(x + k y x y - k)

theorem nat.sub_lt_of_pos_le (a b : ) :
0 < aa bb - 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 : } :
n > 0n.pred.succ = n

theorem nat.sub_eq_zero_of_le {n m : } :
n mn - 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 : } :
n mn + (m - n) = m

theorem nat.sub_add_cancel {n m : } :
n mn - 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 : } :
b a(a - b = c a = c + b)

theorem nat.lt_of_sub_eq_succ {m n l : } :
m - n = l.succn < m

@[simp]
theorem nat.zero_min (a : ) :
min 0 a = 0

@[simp]
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 : ) :
(Π (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 (λ (a : m < n), ih m a) (λ (a : m = n), eq.rec (λ (h₁ : n < n.succ), h n ih) _ h₁)) n)
theorem nat.strong_induction_on {p : → Prop} (n : ) :
(∀ (n : ), (∀ (m : ), m < np m)p n)p n

theorem nat.case_strong_induction_on {p : → Prop} (a : ) :
p 0(∀ (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 : } :
a < ba % b = a

@[simp]
theorem nat.zero_mod (b : ) :
0 % b = 0

theorem nat.mod_eq_sub_mod {a b : } :
a ba % b = (a - b) % b

theorem nat.mod_lt (x : ) {y : } :
y > 0x % 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 : } :
b > 0a ba / b = (a - b) / b + 1

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

theorem nat.le_div_iff_mul_le (x y : ) {k : } :
k > 0(x y / k x * k y)

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

def nat.iterate {α : Sort u} :
(α → α)α → α

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 : } :
n 0(∃ (k : ), n = k.succ)

theorem nat.discriminate {B : Sort u} {n : } :
(n = 0 → B)(Π (m : ), n = m.succ → B) → B

theorem nat.one_succ_zero  :
1 = 1

theorem 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

theorem 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

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 : } :
n + m = 0n = 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 : } :
n mm < nfalse

theorem nat.lt_le_antisymm {n m : } :
n < mm nfalse

theorem nat.lt_asymm {n m : } :
n < m¬m < n

def nat.lt_ge_by_cases {a b : } {C : Sort u} :
(a < b → C)(a b → C) → C

Equations
def nat.lt_by_cases {a b : } {C : Sort u} :
(a < b → C)(a = b → C)(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 : } :
¬a < ba = b b < a

theorem nat.lt_succ_of_lt {a b : } :
a < ba < b.succ

def nat.one_pos  :
0 < 1

theorem nat.sub_le_sub_left {n m : } (k : ) :
n mk - 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 : } :
m nm.succ - n = (m - n).succ

theorem nat.sub_pos_of_lt {m n : } :
m < nn - m > 0

theorem nat.sub_sub_self {n m : } :
m nn - (n - m) = m

theorem nat.sub_add_comm {n m k : } :
k nn + m - k = n - k + m

theorem nat.sub_one_sub_lt {n i : } :
i < nn - 1 - i < n

theorem nat.pred_inj {a b : } :
a > 0b > 0a.pred = b.preda = b

def nat.find_x {p : → Prop} [decidable_pred p] :
(∃ (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] :
(∃ (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 : } :
p mnat.find H 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 : ) :
n * k x(x - n * k) % n = x % n

theorem nat.sub_mul_div (x n p : ) :
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 : } :
z > 0(x + z) / z = (x / z).succ

@[simp]
theorem nat.add_div_left (x : ) {z : } :
z > 0(z + x) / z = (x / z).succ

@[simp]
theorem nat.mul_div_right (n : ) {m : } :
m > 0m * n / m = n

@[simp]
theorem nat.mul_div_left (m : ) {n : } :
n > 0m * n / n = m

@[simp]
theorem nat.div_self {n : } :
n > 0n / n = 1

theorem nat.add_mul_div_left (x z : ) {y : } :
y > 0(x + y * z) / y = x / y + z

theorem nat.add_mul_div_right (x y : ) {z : } :
z > 0(x + y * z) / z = x / z + y

theorem nat.mul_div_cancel (m : ) {n : } :
n > 0m * n / n = m

theorem nat.mul_div_cancel_left (m : ) {n : } :
n > 0n * m / n = m

theorem nat.div_eq_of_eq_mul_left {m n k : } :
n > 0m = k * nm / n = k

theorem nat.div_eq_of_eq_mul_right {m n k : } :
n > 0m = n * km / n = k

theorem nat.div_eq_of_lt_le {m n k : } :
k * n mm < (k.succ) * nm / n = k

theorem nat.mul_sub_div (x n p : ) :
x < n * p(n * p - x.succ) / n = p - (x / n).succ

theorem nat.mul_pos {a b : } :
a > 0b > 0a * b > 0

theorem nat.div_div_eq_div_mul (m n k : ) :
m / n / k = m / n * k

theorem nat.mul_div_mul {m : } (n k : ) :
m > 0m * n / m * k = n / k

@[simp]
theorem nat.dvd_mul_right (a b : ) :
a a * b

theorem nat.dvd_trans {a b c : } :
a bb ca c

theorem nat.eq_zero_of_zero_dvd {a : } :
0 aa = 0

theorem nat.dvd_add {a b c : } :
a ba ca b + c

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

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

theorem nat.dvd_sub {k m n : } :
n mk mk nk m - n

theorem nat.dvd_mod_iff {k m n : } :
k n(k m % n k m)

theorem nat.le_of_dvd {m n : } :
n > 0m nm n

theorem nat.dvd_antisymm {m n : } :
m nn mm = n

theorem nat.pos_of_dvd_of_pos {m n : } :
m nn > 0m > 0

theorem nat.eq_one_of_dvd_one {n : } :
n 1n = 1

theorem nat.dvd_of_mod_eq_zero {m n : } :
n % m = 0m n

theorem nat.mod_eq_zero_of_dvd {m n : } :
m nn % m = 0

theorem nat.dvd_iff_mod_eq_zero (m n : ) :
m n n % m = 0

theorem nat.mul_div_cancel' {m n : } :
n mn * (m / n) = m

theorem nat.div_mul_cancel {m n : } :
n m(m / n) * n = m

theorem nat.mul_div_assoc (m : ) {n k : } :
k nm * n / k = m * (n / k)

theorem nat.dvd_of_mul_dvd_mul_left {m n k : } :
k > 0k * m k * nm n

theorem nat.dvd_of_mul_dvd_mul_right {m n k : } :
k > 0m * k n * km n

theorem nat.mul_le_mul_of_nonneg_left {a b c : } :
a bc * a c * b

theorem nat.mul_le_mul_of_nonneg_right {a b c : } :
a ba * c b * c

theorem nat.mul_lt_mul {a b c d : } :
a < cb d0 < ba * b < c * d

theorem nat.mul_lt_mul' {a b c d : } :
a cb < d0 < ca * b < c * d

theorem nat.mul_le_mul {a b c d : } :
a cb da * b c * d

theorem nat.div_lt_self {n m : } :
n > 0m > 1n / m < n