mathlib3 documentation

core / init.data.nat.basic

inductive nat.less_than_or_equal (a : ) :
Prop
@[protected, instance]
Equations
@[protected, reducible]
def nat.le (n m : ) :
Prop
Equations
@[protected, reducible]
def nat.lt (n m : ) :
Prop
Equations
@[protected, instance]
Equations
def nat.pred  :
Equations
@[protected]
def nat.sub  :
Equations
@[protected]
def nat.mul  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def nat.repeat {α : Type u} (f : α α) :
α α
Equations
@[protected, instance]
Equations
@[simp]
theorem nat.nat_zero_eq_zero  :
0 = 0

properties of inequality

@[protected, refl]
theorem nat.le_refl (a : ) :
a a
theorem nat.le_succ (n : ) :
n n.succ
theorem nat.succ_le_succ {n m : } :
n m n.succ m.succ
@[protected]
theorem nat.zero_le (n : ) :
0 n
theorem nat.zero_lt_succ (n : ) :
0 < n.succ
theorem nat.succ_pos (n : ) :
0 < n.succ
@[protected, simp]
theorem nat.not_lt_zero (a : ) :
¬a < 0
theorem nat.pred_le_pred {n m : } :
n m n.pred m.pred
theorem nat.le_of_succ_le_succ {n m : } :
n.succ m.succ n m
@[protected, instance]
def nat.decidable_le (a b : ) :
Equations
@[protected, instance]
def nat.decidable_lt (a b : ) :
decidable (a < b)
Equations
@[protected]
theorem nat.eq_or_lt_of_le {a b : } (h : a b) :
a = b a < b
theorem nat.lt_succ_of_le {a b : } :
a b a < 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 : ) :
@[protected]
theorem nat.lt_irrefl (n : ) :
¬n < n
@[protected]
theorem nat.le_trans {n m k : } (h1 : n m) :
m k n k
theorem nat.pred_le (n : ) :
n.pred n
theorem nat.pred_lt {n : } :
n 0 n.pred < n
@[protected]
theorem nat.sub_le (a b : ) :
a - b a
@[protected]
theorem nat.sub_lt {a b : } :
0 < a 0 < b a - b < a
@[protected]
theorem nat.lt_of_lt_of_le {n m k : } :
n < m m k n < k

Basic nat.add lemmas

@[protected]
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
@[protected]
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

Basic lemmas for comparing numerals

@[protected]
theorem nat.bit0_succ_eq (n : ) :
@[protected]
theorem nat.zero_lt_bit0 {n : } :
n 0 0 < bit0 n
@[protected]
theorem nat.zero_lt_bit1 (n : ) :
0 < bit1 n
@[protected]
theorem nat.bit0_ne_zero {n : } :
n 0 bit0 n 0
@[protected, simp]
theorem nat.bit1_ne_zero (n : ) :
bit1 n 0