Library Coq.Init.Peano
The type
nat of Peano natural numbers (built from
O and
S)
is defined in
Datatypes.v
This module defines the following operations on natural numbers :
- predecessor pred
- addition plus
- multiplication mult
- less or equal order le
- less lt
- greater or equal ge
- greater gt
It states various lemmas and theorems about natural numbers,
including Peano's axioms of arithmetic (in Coq, these are provable).
Case analysis on
nat and induction on
nat * nat are provided too
The predecessor function
Injectivity of successor
Zero is not the successor of a number
Theorem O_S :
forall n:
nat, 0
<> S n.
Hint Resolve O_S:
core.
Theorem n_Sn :
forall n:
nat,
n <> S n.
Hint Resolve n_Sn:
core.
Addition
Standard associated names
Multiplication
Standard associated names
Truncated subtraction: m-n is 0 if n>=m
Definition of the usual orders, the basic properties of le and lt
can be found in files Le and Lt
Case analysis
Principle of double induction
Maximum and minimum : definitions and specifications