diff options
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 9c6fcf1d..08a416c1 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne |