mathlib documentation

core.init.data.nat.basic

inductive nat.less_than_or_equal  :
→ Prop

@[instance]

Equations
def nat.le  :
→ Prop

Equations
def nat.lt  :
→ Prop

Equations
@[instance]

Equations
def nat.pred  :

Equations
def nat.sub  :

Equations
def nat.mul  :

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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

Equations
@[instance]

Equations
@[simp]
theorem nat.nat_zero_eq_zero  :
0 = 0

def nat.le_refl (a : ) :
a a

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

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

theorem nat.zero_le (n : ) :
0 n

theorem nat.zero_lt_succ (n : ) :
0 < n.succ

def nat.succ_pos (n : ) :
0 < n.succ

theorem nat.not_succ_le_zero (n : ) :
n.succ 0false

theorem nat.not_lt_zero (a : ) :
¬a < 0

theorem nat.pred_le_pred {n m : } :
n mn.pred m.pred

theorem nat.le_of_succ_le_succ {n m : } :
n.succ m.succn m

@[instance]
def nat.decidable_le (a b : ) :

Equations
@[instance]
def nat.decidable_lt (a b : ) :
decidable (a < b)

Equations
theorem nat.eq_or_lt_of_le {a b : } :
a ba = b a < b

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

@[simp]
theorem nat.succ_sub_succ_eq_sub (a b : ) :
a.succ - b.succ = a - b

theorem nat.not_succ_le_self (n : ) :

theorem nat.lt_irrefl (n : ) :
¬n < n

theorem nat.le_trans {n m k : } :
n mm kn k

theorem nat.pred_le (n : ) :
n.pred n

theorem nat.pred_lt {n : } :
n 0n.pred < n

theorem nat.sub_le (a b : ) :
a - b a

theorem nat.sub_lt {a b : } :
0 < a0 < ba - b < a

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

theorem nat.zero_add (n : ) :
0 + n = n

theorem nat.succ_add (n m : ) :
n.succ + m = (n + m).succ

theorem nat.add_succ (n m : ) :
n + m.succ = (n + m).succ

theorem nat.add_zero (n : ) :
n + 0 = n

theorem nat.add_one (n : ) :
n + 1 = n.succ

theorem nat.succ_eq_add_one (n : ) :
n.succ = n + 1

theorem nat.bit0_succ_eq (n : ) :

theorem nat.zero_lt_bit0 {n : } :
n 00 < bit0 n

theorem nat.zero_lt_bit1 (n : ) :
0 < bit1 n

theorem nat.bit0_ne_zero {n : } :
n 0bit0 n 0

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