diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-10 11:19:21 +0000 |
| commit | 424b20ed34966506cef31abf85e3e3911138f0fc (patch) | |
| tree | 6239f8c02d629b5ccff23213dc1ff96dd040688b /theories/ZArith/BinInt.v | |
| parent | e03541b7092e136edc78335cb178c0217dd48bc5 (diff) | |
DecidableType: A specification via boolean equality as an alternative to eq_dec
+ adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
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 06ba2eb89..d976b01c6 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. |