Library Coq.Arith.Peano_dec
Require
Import
Decidable
PeanoNat
.
Require
Eqdep_dec
.
Local Open
Scope
nat_scope
.
Implicit
Types
m
n
x
y
:
nat
.
Theorem
O_or_S
n
:
{
m
:
nat
|
S
m
=
n
}
+
{
0
=
n
}
.
Notation
eq_nat_dec
:=
Nat.eq_dec
(
only
parsing
).
Hint Resolve
O_or_S
eq_nat_dec
:
arith
.
Theorem
dec_eq_nat
n
m
:
decidable
(
n
=
m
).
Definition
UIP_nat
:=
Eqdep_dec.UIP_dec
Nat.eq_dec
.
Import
EqNotations
.
Lemma
le_unique
:
forall
m
n
(
le_mn1
le_mn2
:
m
<=
n
),
le_mn1
=
le_mn2
.
For compatibility
Require
Import
Le
Lt
.