diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rwxr-xr-x | theories/Arith/Compare_dec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 531e0a9754..f9e93b9bf9 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -55,7 +55,7 @@ Intros; Elim (lt_eq_lt_dec n m); Auto with arith. Intros; Absurd (lt m n); Auto with arith. Qed. -(* Proofs of decidability *) +(** Proofs of decidability *) Theorem dec_le:(x,y:nat)(decidable (le x y)). Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ |