Library Coq.Arith.Compare_dec
Require Import Le.
Require Import Lt.
Require Import Gt.
Require Import Decidable.
Open Local Scope nat_scope.
Implicit Types m n x y :
nat.
Definition zerop n : {
n = 0} + {0 <
n}.
Defined.
Definition lt_eq_lt_dec n m : {
n <
m} + {
n =
m} + {
m <
n}.
Defined.
Definition gt_eq_gt_dec n m : {
m >
n} + {
n =
m} + {
n >
m}.
Defined.
Definition le_lt_dec n m : {
n <=
m} + {
m <
n}.
Defined.
Definition le_le_S_dec n m : {
n <=
m} + {
S m <=
n}.
Defined.
Definition le_ge_dec n m : {
n <=
m} + {
n >=
m}.
Defined.
Definition le_gt_dec n m : {
n <=
m} + {
n >
m}.
Defined.
Definition le_lt_eq_dec n m :
n <=
m -> {
n <
m} + {
n =
m}.
Defined.
Proofs of decidability
A ternary comparison function in the spirit of Zcompare.
A boolean version of le over nat.