Add decidability instances for Z.gt and Z.ge

583c4645 · Tej Chajed · Robbert Krebbers · 355c84cf · 583c4645
Commit 583c4645 authored Feb 13, 2020 by Tej Chajed Committed by Robbert Krebbers Feb 13, 2020
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/numbers.v theories/numbers.v +2 -0

No files found.
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -368,6 +368,8 @@ Proof. intros n1 n2. apply Nat2Z.inj. Qed.
 Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
 Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
 Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
+Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
+Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
 Instance Z_inhabited: Inhabited Z := populate 1.
 Instance Z_lt_pi x y : ProofIrrel (x < y).
 Proof. unfold Z.lt. apply _. Qed.