core / init.data.nat.basic

source

inductive nat.less_than_or_equal (a : ℕ) :

ℕ → Prop

refl : ∀ {a : ℕ}, a.less_than_or_equal a
step : ∀ {a b : ℕ}, a.less_than_or_equal b → a.less_than_or_equal b.succ

source

@[protected, instance]

def nat.has_le :

has_le ℕ

Equations

nat.has_le = {le := nat.less_than_or_equal}

source

@[protected, reducible]

def nat.le (n m : ℕ) :

Prop

Equations

n.le m = n.less_than_or_equal m

source

@[protected, reducible]

def nat.lt (n m : ℕ) :

Prop

Equations

n.lt m = n.succ.less_than_or_equal m

source

@[protected, instance]

def nat.has_lt :

has_lt ℕ

Equations

nat.has_lt = {lt := nat.lt}

source

def nat.pred :

ℕ → ℕ

Equations

(a + 1).pred = a
0.pred = 0

source

@[protected]

def nat.sub :

ℕ → ℕ → ℕ

Equations

a.sub (b + 1) = (a.sub b).pred
a.sub 0 = a

source

@[protected]

def nat.mul :

ℕ → ℕ → ℕ

Equations

a.mul (b + 1) = a.mul b + a
a.mul 0 = 0

source

@[protected, instance]

def nat.has_sub :

has_sub ℕ

Equations

nat.has_sub = {sub := nat.sub}

source

@[protected, instance]

def nat.has_mul :

has_mul ℕ

Equations

nat.has_mul = {mul := nat.mul}

source

@[protected, instance]

def nat.has_dvd :

has_dvd ℕ

Equations

nat.has_dvd = {dvd := λ (a b : ℕ), ∃ (c : ℕ), b = a * c}

source

@[protected, instance]

def nat.decidable_eq :

decidable_eq ℕ

Equations

nat.decidable_eq x.succ y.succ = nat.decidable_eq._match_1 x y (nat.decidable_eq x y)
nat.decidable_eq x.succ 0 = decidable.is_false _
nat.decidable_eq 0 y.succ = decidable.is_false _
nat.decidable_eq 0 0 = decidable.is_true rfl
nat.decidable_eq._match_1 x y (decidable.is_true xeqy) = decidable.is_true _
nat.decidable_eq._match_1 x y (decidable.is_false xney) = decidable.is_false _

source

def nat.repeat {α : Type u} (f : ℕ → α → α) :

ℕ → α → α

Equations

nat.repeat f n.succ a = f n (nat.repeat f n a)
nat.repeat f 0 a = a

source

@[protected, instance]

def nat.inhabited :

inhabited ℕ

Equations

nat.inhabited = {default := 0}

source

@[simp]

theorem nat.nat_zero_eq_zero :

0 = 0

source

@[protected, refl]

theorem nat.le_refl (a : ℕ) :

a ≤ a

source

theorem nat.le_succ (n : ℕ) :

n ≤ n.succ

source

theorem nat.succ_le_succ {n m : ℕ} :

n ≤ m → n.succ ≤ m.succ

source

@[protected]

theorem nat.zero_le (n : ℕ) :

0 ≤ n

source

theorem nat.zero_lt_succ (n : ℕ) :

0 < n.succ

source

theorem nat.succ_pos (n : ℕ) :

0 < n.succ

source

theorem nat.not_succ_le_zero (n : ℕ) :

n.succ ≤ 0 → false

source

@[protected, simp]

theorem nat.not_lt_zero (a : ℕ) :

¬a < 0

source

theorem nat.pred_le_pred {n m : ℕ} :

n ≤ m → n.pred ≤ m.pred

source

theorem nat.le_of_succ_le_succ {n m : ℕ} :

n.succ ≤ m.succ → n ≤ m

source

@[protected, instance]

def nat.decidable_le (a b : ℕ) :

decidable (a ≤ b)

Equations

(a + 1).decidable_le (b + 1) = nat.decidable_le._match_1 a b (a.decidable_le b)
(a + 1).decidable_le 0 = decidable.is_false _
0.decidable_le b = decidable.is_true _
nat.decidable_le._match_1 a b (decidable.is_true h) = decidable.is_true _
nat.decidable_le._match_1 a b (decidable.is_false h) = decidable.is_false _

source

@[protected, instance]

def nat.decidable_lt (a b : ℕ) :

decidable (a < b)

Equations

nat.decidable_lt = λ (a b : ℕ), a.succ.decidable_le b

source

@[protected]

theorem nat.eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) :

a = b ∨ a < b

source

theorem nat.lt_succ_of_le {a b : ℕ} :

a ≤ b → a < b.succ

source

@[simp]

theorem nat.succ_sub_succ_eq_sub (a b : ℕ) :

a.succ - b.succ = a - b

source

theorem nat.not_succ_le_self (n : ℕ) :

¬n.succ ≤ n

source

@[protected]

theorem nat.lt_irrefl (n : ℕ) :

¬n < n

source

@[protected]

theorem nat.le_trans {n m k : ℕ} (h1 : n ≤ m) :

m ≤ k → n ≤ k

source

theorem nat.pred_le (n : ℕ) :

n.pred ≤ n

source

theorem nat.pred_lt {n : ℕ} :

n ≠ 0 → n.pred < n

source

@[protected]

theorem nat.sub_le (a b : ℕ) :

a - b ≤ a

source

@[protected]

theorem nat.sub_lt {a b : ℕ} :

0 < a → 0 < b → a - b < a

source

@[protected]

theorem nat.lt_of_lt_of_le {n m k : ℕ} :

n < m → m ≤ k → n < k

source

@[protected]

theorem nat.zero_add (n : ℕ) :

0 + n = n

source

theorem nat.succ_add (n m : ℕ) :

n.succ + m = (n + m).succ

source

theorem nat.add_succ (n m : ℕ) :

n + m.succ = (n + m).succ

source

@[protected]

theorem nat.add_zero (n : ℕ) :

n + 0 = n

source

theorem nat.add_one (n : ℕ) :

n + 1 = n.succ

source

theorem nat.succ_eq_add_one (n : ℕ) :

n.succ = n + 1

source

@[protected]

theorem nat.bit0_succ_eq (n : ℕ) :

bit0 n.succ = (bit0 n).succ.succ

source

@[protected]

theorem nat.zero_lt_bit0 {n : ℕ} :

n ≠ 0 → 0 < bit0 n

source

@[protected]

theorem nat.zero_lt_bit1 (n : ℕ) :

0 < bit1 n

source

@[protected]

theorem nat.bit0_ne_zero {n : ℕ} :

n ≠ 0 → bit0 n ≠ 0

source

@[protected, simp]

theorem nat.bit1_ne_zero (n : ℕ) :

bit1 n ≠ 0