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
Operation x -> 2*x+1
Operation x -> 2*x
Successor
Predecessor
Addition
Subtraction
Multiplication
Boolean Equality
Order
Min and max
Decidability of equality.
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 boolean order.
Properties of comparison
Lemma Ncompare_refl :
forall n,
(n ?= n) = Eq.
Theorem Ncompare_Eq_eq :
forall n m:
N,
(n ?= m) = Eq ->
n = m.
Theorem Ncompare_eq_correct :
forall n m:
N,
(n ?= m) = Eq <-> n = m.
Lemma Ncompare_antisym :
forall n m,
CompOpp (
n ?= m)
= (m ?= n).
Lemma Ngt_Nlt :
forall n m,
n > m ->
m < n.
Theorem Nlt_irrefl :
forall n :
N,
~ n < n.
Theorem Nlt_trans :
forall n m q,
n < m ->
m < q ->
n < q.
Theorem Nlt_not_eq :
forall n m,
n < m ->
~ n = m.
Theorem Ncompare_n_Sm :
forall n m :
N,
Ncompare n (
Nsucc m)
= Lt <-> Ncompare n m = Lt \/ n = m.
Lemma Nle_lteq :
forall x y,
x <= y <-> x < y \/ x=y.
Lemma Ncompare_spec :
forall x y,
CompSpec eq Nlt x y (
Ncompare x y).
0 is the least natural number
Dividing by 2