diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index fe37fccb8..a32ccbc4b 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -97,7 +97,7 @@ Proof. unfold "?=". intros. apply Zcompare_antisym. Qed. -Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y). +Lemma Qcompare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (x ?= y). Proof. intros. destruct (x ?= y) as [ ]_eqn:H; constructor; auto. |