Library Coq.Arith.Compare
Equality is decidable on
nat
Local
Open
Scope
nat_scope
.
Notation
not_eq_sym
:=
not_eq_sym
(
only
parsing
).
Implicit
Types
m
n
p
q
:
nat
.
Require
Import
Arith_base
.
Require
Import
Peano_dec
.
Require
Import
Compare_dec
.
Definition
le_or_le_S
:=
le_le_S_dec
.
Definition
Pcompare
:=
gt_eq_gt_dec
.
Lemma
le_dec
:
forall
n
m
,
{
n
<=
m
}
+
{
m
<=
n
}
.
Definition
lt_or_eq
n
m
:=
{
m
>
n
}
+
{
n
=
m
}
.
Lemma
le_decide
:
forall
n
m
,
n
<=
m
->
lt_or_eq
n
m
.
Lemma
le_le_S_eq
:
forall
n
m
,
n
<=
m
->
S
n
<=
m
\/
n
=
m
.
Lemma
discrete_nat
:
forall
n
m
,
n
<
m
->
S
n
=
m
\/
(
exists
r
:
nat
,
m
=
S
(
S
(
n
+
r
))
)
.
Require
Export
Wf_nat
.
Require
Export
Min
Max
.