diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index cef8c38198..bff52fb37f 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -126,7 +126,7 @@ Qed. (** Order *) -Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). Proof. intros. zify. destruct (Zcompare_spec [x] [y]); auto. Qed. |