Library Coq.Arith.Peano_dec
Require
Import
Decidable
.
Open
Local
Scope
nat_scope
.
Implicit
Types
m
n
x
y
:
nat
.
Theorem
O_or_S
:
forall
n
, {
m
:
nat
|
S
m
=
n
} + {0 =
n
}.
Theorem
eq_nat_dec
:
forall
n
m
, {
n
=
m
} + {
n
<>
m
}.
Hint
Resolve
O_or_S
eq_nat_dec
:
arith
.
Theorem
dec_eq_nat
:
forall
n
m
,
decidable
(
n
=
m
).