Library Coq.NArith.BinNat
Binary natural numbers
Declare binding key for scope positive_scope
Delimit Scope N_scope with N.
Automatically open scope positive_scope for the constructors of N
Open Local Scope N_scope.
Definition Ndiscr :
forall n:N, {
p:positive |
n =
Npos p } + {
n =
N0 }.
Operation x -> 2*x+1
Operation x -> 2*x
Successor
Predecessor
Addition
Definition Nplus n m :=
match n,
m with
|
N0,
_ =>
m
|
_,
N0 =>
n
|
Npos p,
Npos q =>
Npos (
p +
q)
end.
Infix "+" :=
Nplus :
N_scope.
Subtraction
Multiplication
Order
Definition Ncompare n m :=
match n,
m with
|
N0,
N0 =>
Eq
|
N0,
Npos m' =>
Lt
|
Npos n',
N0 =>
Gt
|
Npos n',
Npos m' => (
n' ?=
m')%positive
Eq
end.
Infix "?=" :=
Ncompare (
at level 70,
no associativity) :
N_scope.
Definition Nlt (
x y:N) := (
x ?=
y) =
Lt.
Definition Ngt (
x y:N) := (
x ?=
y) =
Gt.
Definition Nle (
x y:N) := (
x ?=
y) <>
Gt.
Definition Nge (
x y:N) := (
x ?=
y) <>
Lt.
Infix "<=" :=
Nle :
N_scope.
Infix "<" :=
Nlt :
N_scope.
Infix ">=" :=
Nge :
N_scope.
Infix ">" :=
Ngt :
N_scope.
Min and max
convenient induction principles
Peano induction on binary natural numbers
Properties of successor and predecessor
Properties of addition
Properties of subtraction.
Properties of multiplication
Properties of comparison
0 is the least natural number
Dividing by 2