diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 06ba2eb89b..d976b01c6b 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -226,6 +226,11 @@ Qed. (** ** Properties of opposite on binary integer numbers *) +Theorem Zopp_0 : Zopp Z0 = Z0. +Proof. + reflexivity. +Qed. + Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. Proof. reflexivity. |