The Coq Proof Assistant

# 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).
#[global]
Hint Resolve O_or_S eq_nat_dec: arith.
Theorem dec_eq_nat n m : decidable (n = m).
Register dec_eq_nat as num.nat.eq_dec.
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.