mathlib documentation

core / init.data.nat.lemmas

addition

@[protected]
theorem nat.add_comm (n m : ) :
n + m = m + n
@[protected]
theorem nat.add_assoc (n m k : ) :
n + m + k = n + (m + k)
@[protected]
theorem nat.add_left_comm (n m k : ) :
n + (m + k) = m + (n + k)
@[protected]
theorem nat.add_left_cancel {n m k : } :
n + m = n + km = k
@[protected]
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
@[protected, simp]
theorem nat.one_ne_zero  :
1 0
@[protected, simp]
theorem nat.zero_ne_one  :
0 1
@[protected]
theorem nat.eq_zero_of_add_eq_zero_right {n m : } :
n + m = 0n = 0
@[protected]
theorem nat.eq_zero_of_add_eq_zero_left {n m : } (h : n + m = 0) :
m = 0
@[protected]
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

multiplication

@[protected]
theorem nat.mul_zero (n : ) :
n * 0 = 0
theorem nat.mul_succ (n m : ) :
n * m.succ = n * m + n
@[protected]
theorem nat.zero_mul (n : ) :
0 * n = 0
theorem nat.succ_mul (n m : ) :
(n.succ) * m = n * m + m
@[protected]
theorem nat.right_distrib (n m k : ) :
(n + m) * k = n * k + m * k
@[protected]
theorem nat.left_distrib (n m k : ) :
n * (m + k) = n * m + n * k
@[protected]
theorem nat.mul_comm (n m : ) :
n * m = m * n
@[protected]
theorem nat.mul_assoc (n m k : ) :
(n * m) * k = n * m * k
@[protected]
theorem nat.mul_one (n : ) :
n * 1 = n
@[protected]
theorem nat.one_mul (n : ) :
1 * n = n
theorem nat.succ_add_eq_succ_add (n m : ) :
n.succ + m = n + m.succ
theorem nat.eq_zero_of_mul_eq_zero {n m : } :
n * m = 0n = 0 m = 0

properties of inequality

@[protected]
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
@[protected]
theorem nat.le_of_lt {n m : } (h : n < m) :
n m
theorem nat.lt.step {n m : } :
n < mn < m.succ
@[protected]
theorem nat.eq_zero_or_pos (n : ) :
n = 0 0 < n
@[protected]
theorem nat.pos_of_ne_zero {n : } :
n 00 < n
@[protected]
theorem nat.lt_trans {n m k : } (h₁ : n < m) :
m < kn < k
@[protected]
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
@[protected]
theorem nat.le_antisymm {n m : } (h₁ : n m) :
m nn = m
@[protected]
theorem nat.lt_or_ge (a b : ) :
a < b b a
@[protected]
theorem nat.le_total {m n : } :
m n n m
@[protected]
theorem nat.lt_of_le_and_ne {m n : } (h1 : m n) :
m nm < n
@[protected]
theorem nat.lt_iff_le_not_le {m n : } :
m < n m n ¬n m
@[protected]
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
@[protected]
theorem nat.le_add_right (n k : ) :
n n + k
@[protected]
theorem nat.le_add_left (n m : ) :
n m + n
theorem nat.le.dest {n m : } :
n m(∃ (k : ), n + k = m)
@[protected]
theorem nat.le.intro {n m k : } (h : n + k = m) :
n m
@[protected]
theorem nat.add_le_add_left {n m : } (h : n m) (k : ) :
k + n k + m
@[protected]
theorem nat.add_le_add_right {n m : } (h : n m) (k : ) :
n + k m + k
@[protected]
theorem nat.le_of_add_le_add_left {k n m : } (h : k + n k + m) :
n m
@[protected]
theorem nat.le_of_add_le_add_right {k n m : } :
n + k m + kn m
@[protected]
theorem nat.add_le_add_iff_le_right (k n m : ) :
n + k m + k n m
@[protected]
theorem nat.lt_of_add_lt_add_left {k n m : } (h : k + n < k + m) :
n < m
@[protected]
theorem nat.lt_of_add_lt_add_right {a b c : } (h : a + b < c + b) :
a < c
@[protected]
theorem nat.add_lt_add_left {n m : } (h : n < m) (k : ) :
k + n < k + m
@[protected]
theorem nat.add_lt_add_right {n m : } (h : n < m) (k : ) :
n + k < m + k
@[protected]
theorem nat.lt_add_of_pos_right {n k : } (h : 0 < k) :
n < n + k
@[protected]
theorem nat.lt_add_of_pos_left {n k : } (h : 0 < k) :
n < k + n
@[protected]
theorem nat.add_lt_add {a b c d : } (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
@[protected]
theorem nat.add_le_add {a b c d : } (h₁ : a b) (h₂ : c d) :
a + c b + d
@[protected]
theorem nat.zero_lt_one  :
0 < 1
@[protected]
theorem nat.mul_le_mul_left {n m : } (k : ) (h : n m) :
k * n k * m
@[protected]
theorem nat.mul_le_mul_right {n m : } (k : ) (h : n m) :
n * k m * k
@[protected]
theorem nat.mul_lt_mul_of_pos_left {n m k : } (h : n < m) (hk : 0 < k) :
k * n < k * m
@[protected]
theorem nat.mul_lt_mul_of_pos_right {n m k : } (h : n < m) (hk : 0 < k) :
n * k < m * k
@[protected]
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
@[protected]
theorem nat.eq_of_mul_eq_mul_left {m k n : } (Hn : 0 < n) (H : n * m = n * k) :
m = k
@[protected]
theorem nat.mul_pos {a b : } (ha : 0 < a) (hb : 0 < b) :
0 < a * b
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) :
@[protected]
theorem nat.lt_asymm {n m : } (h₁ : n < m) :
¬m < n
@[protected]
def nat.lt_ge_by_cases {a b : } {C : Sort u} (h₁ : a < b → C) (h₂ : b a → C) :
C
Equations
@[protected]
def nat.lt_by_cases {a b : } {C : Sort u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) :
C
Equations
@[protected]
theorem nat.lt_trichotomy (a b : ) :
a < b a = b b < a
@[protected]
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
@[protected]
theorem nat.mul_le_mul_of_nonneg_left {a b c : } (h₁ : a b) :
c * a c * b
@[protected]
theorem nat.mul_le_mul_of_nonneg_right {a b c : } (h₁ : a b) :
a * c b * c
@[protected]
theorem nat.mul_lt_mul {a b c d : } (hac : a < c) (hbd : b d) (pos_b : 0 < b) :
a * b < c * d
@[protected]
theorem nat.mul_lt_mul' {a b c d : } (h1 : a c) (h2 : b < d) (h3 : 0 < c) :
a * b < c * d
@[protected]
theorem nat.mul_le_mul {a b c d : } (hac : a c) (hbd : b d) :
a * b c * d

bit0/bit1 properties

@[protected]
theorem nat.bit1_eq_succ_bit0 (n : ) :
bit1 n = (bit0 n).succ
@[protected]
theorem nat.bit1_succ_eq (n : ) :
@[protected]
theorem nat.bit1_ne_one {n : } :
n 0bit1 n 1
@[protected, simp]
theorem nat.bit0_ne_one (n : ) :
bit0 n 1
@[protected]
theorem nat.add_self_ne_one (n : ) :
n + n 1
@[protected, simp]
theorem nat.bit1_ne_bit0 (n m : ) :
@[protected, simp]
theorem nat.bit0_ne_bit1 (n m : ) :
@[protected]
theorem nat.bit0_inj {n m : } :
bit0 n = bit0 mn = m
@[protected]
theorem nat.bit1_inj {n m : } :
bit1 n = bit1 mn = m
@[protected]
theorem nat.bit0_ne {n m : } :
n mbit0 n bit0 m
@[protected]
theorem nat.bit1_ne {n m : } :
n mbit1 n bit1 m
@[protected]
theorem nat.zero_ne_bit0 {n : } :
n 00 bit0 n
@[protected, simp]
theorem nat.zero_ne_bit1 (n : ) :
0 bit1 n
@[protected, simp]
theorem nat.one_ne_bit0 (n : ) :
1 bit0 n
@[protected]
theorem nat.one_ne_bit1 {n : } :
n 01 bit1 n
@[protected]
theorem nat.one_lt_bit1 {n : } :
n 01 < bit1 n
@[protected]
theorem nat.one_lt_bit0 {n : } :
n 01 < bit0 n
@[protected]
theorem nat.bit0_lt {n m : } (h : n < m) :
bit0 n < bit0 m
@[protected]
theorem nat.bit1_lt {n m : } (h : n < m) :
bit1 n < bit1 m
@[protected]
theorem nat.bit0_lt_bit1 {n m : } (h : n m) :
bit0 n < bit1 m
@[protected]
theorem nat.bit1_lt_bit0 {n m : } :
n < mbit1 n < bit0 m
@[protected]
theorem nat.one_le_bit1 (n : ) :
1 bit1 n
@[protected]
theorem nat.one_le_bit0 (n : ) :
n 01 bit0 n

successor and predecessor

@[simp]
theorem nat.pred_zero  :
0.pred = 0
@[simp]
theorem nat.pred_succ (n : ) :
n.succ.pred = n
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
theorem nat.pred_inj {a b : } :
0 < a0 < ba.pred = b.preda = b

subtraction

Many lemmas are proven more generally in mathlib algebra/order/sub

@[protected, simp]
theorem nat.zero_sub (a : ) :
0 - a = 0
theorem nat.sub_lt_succ (a b : ) :
a - b < a.succ
@[protected]
theorem nat.sub_le_sub_right {n m : } (h : n m) (k : ) :
n - k m - k
@[protected, 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
@[protected]
theorem nat.sub_self (n : ) :
n - n = 0
@[protected]
theorem nat.add_sub_add_right (n k m : ) :
n + k - (m + k) = n - m
@[protected]
theorem nat.add_sub_add_left (k n m : ) :
k + n - (k + m) = n - m
@[protected]
theorem nat.add_sub_cancel (n m : ) :
n + m - m = n
@[protected]
theorem nat.add_sub_cancel_left (n m : ) :
n + m - n = m
@[protected]
theorem nat.sub_sub (n m k : ) :
n - m - k = n - (m + k)
@[protected]
theorem nat.le_of_le_of_sub_le_sub_right {n m k : } (h₀ : k m) (h₁ : n - k m - k) :
n m
@[protected]
theorem nat.sub_le_sub_right_iff (n m k : ) (h : k m) :
n - k m - k n m
@[protected]
theorem nat.sub_self_add (n m : ) :
n - (n + m) = 0
@[protected]
theorem nat.add_le_to_le_sub (x : ) {y k : } (h : k y) :
x + k y x y - k
@[protected]
theorem nat.sub_lt_of_pos_le (a b : ) (h₀ : 0 < a) (h₁ : a b) :
b - a < b
@[protected]
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
@[protected]
theorem nat.sub_eq_zero_of_le {n m : } (h : n m) :
n - m = 0
@[protected]
theorem nat.le_of_sub_eq_zero {n m : } :
n - m = 0n m
@[protected]
theorem nat.sub_eq_zero_iff_le {n m : } :
n - m = 0 n m
@[protected]
theorem nat.add_sub_of_le {n m : } (h : n m) :
n + (m - n) = m
@[protected]
theorem nat.sub_add_cancel {n m : } (h : m n) :
n - m + m = n
@[protected]
theorem nat.add_sub_assoc {m k : } (h : k m) (n : ) :
n + m - k = n + (m - k)
@[protected]
theorem nat.sub_eq_iff_eq_add {a b c : } (ab : b a) :
a - b = c a = c + b
@[protected]
theorem nat.lt_of_sub_eq_succ {m n l : } (H : m - n = l.succ) :
n < m
@[protected]
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
@[protected]
theorem nat.sub.right_comm (m n k : ) :
m - n - k = m - k - n
theorem nat.succ_sub {m n : } (h : n m) :
m.succ - n = (m - n).succ
@[protected]
theorem nat.sub_pos_of_lt {m n : } (h : m < n) :
0 < n - m
@[protected]
theorem nat.sub_sub_self {n m : } (h : m n) :
n - (n - m) = m
@[protected]
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.mul_pred_left (n m : ) :
(n.pred) * m = n * m - m
theorem nat.mul_pred_right (n m : ) :
n * m.pred = n * m - n
@[protected]
theorem nat.mul_sub_right_distrib (n m k : ) :
(n - m) * k = n * k - m * k
@[protected]
theorem nat.mul_sub_left_distrib (n m k : ) :
n * (m - k) = n * m - n * k
@[protected]
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

min

@[protected]
theorem nat.zero_min (a : ) :
min 0 a = 0
@[protected]
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
@[protected, simp]
theorem nat.sub_add_min_cancel (n m : ) :
n - m + min n m = n

induction principles

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
@[protected]
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)
@[protected]
theorem nat.strong_induction_on {p : → Prop} (n : ) (h : ∀ (n : ), (∀ (m : ), m < np m)p n) :
p n
@[protected]
theorem nat.case_strong_induction_on {p : → Prop} (a : ) (hz : p 0) (hi : ∀ (n : ), (∀ (m : ), m np m)p n.succ) :
p a

mod

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.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

div

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
@[protected, simp]
theorem nat.div_one (n : ) :
n / 1 = n
@[protected, simp]
theorem nat.div_zero (n : ) :
n / 0 = 0
@[protected, simp]
theorem nat.zero_div (b : ) :
0 / b = 0
@[protected]
theorem nat.div_le_of_le_mul {m n k : } :
m k * nm / k n
@[protected]
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
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
@[protected, 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
@[protected]
theorem nat.mul_div_cancel (m : ) {n : } (H : 0 < n) :
m * n / n = m
@[protected]
theorem nat.mul_div_cancel_left (m : ) {n : } (H : 0 < n) :
n * m / n = m
@[protected]
theorem nat.div_eq_of_eq_mul_left {m n k : } (H1 : 0 < n) (H2 : m = k * n) :
m / n = k
@[protected]
theorem nat.div_eq_of_eq_mul_right {m n k : } (H1 : 0 < n) (H2 : m = n * k) :
m / n = k
@[protected]
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
@[protected]
theorem nat.div_div_eq_div_mul (m n k : ) :
m / n / k = m / n * k
@[protected]
theorem nat.mul_div_mul {m : } (n k : ) (H : 0 < m) :
m * n / m * k = n / k
theorem nat.div_lt_self {n m : } :
0 < n1 < mn / m < n

dvd

@[protected]
theorem nat.dvd_mul_right (a b : ) :
a a * b
@[protected]
theorem nat.dvd_trans {a b c : } (h₁ : a b) (h₂ : b c) :
a c
@[protected]
theorem nat.eq_zero_of_zero_dvd {a : } (h : 0 a) :
a = 0
@[protected]
theorem nat.dvd_add {a b c : } (h₁ : a b) (h₂ : a c) :
a b + c
@[protected]
theorem nat.dvd_add_iff_right {k m n : } (h : k m) :
k n k m + n
@[protected]
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
@[protected, instance]
Equations
@[protected]
theorem nat.mul_div_cancel' {m n : } (H : n m) :
n * (m / n) = m
@[protected]
theorem nat.div_mul_cancel {m n : } (H : n m) :
(m / n) * n = m
@[protected]
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

iterate

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

find

@[protected]
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
@[protected]
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
@[protected]
theorem nat.find_spec {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) :
p (nat.find H)
@[protected]
theorem nat.find_min {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) {m : } :
m < nat.find H¬p m
@[protected]
theorem nat.find_min' {p : → Prop} [decidable_pred p] (H : ∃ (n : ), p n) {m : } (h : p m) :