diff options
Diffstat (limited to 'theories/PArith/BinPos.v')
| -rw-r--r-- | theories/PArith/BinPos.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 64e32c560..4570fde72 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1015,7 +1015,7 @@ Proof. symmetry; apply Pcompare_antisym. Qed. -Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq). +Lemma Pcompare_spec : forall p q, CompareSpec (p=q) (p<q) (q<p) ((p ?= q) Eq). Proof. intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor. apply Pcompare_Eq_eq; auto. |