diff options
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index cb8ac3b5b1..0a52d214a2 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -132,7 +132,14 @@ Qed. End NZOrdAxiomsMod. -Definition Zopp := Zopp. +Definition Zopp (x : Z) := +match x with +| Z0 => Z0 +| Zpos x => Zneg x +| Zneg x => Zpos x +end. + +Notation "- x" := (Zopp x) : Z_scope. Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd. Proof. |