diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 686a0692c..3f256b40f 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -547,7 +547,7 @@ Proof. intuition; now try discriminate V. Qed. -Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y). +Lemma Ncompare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (x ?= y). Proof. intros. destruct (Ncompare x y) as [ ]_eqn; constructor; auto. |