diff options
| author | herbelin | 2003-11-21 22:34:05 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-21 22:34:05 +0000 |
| commit | 8769d8ec01eaca509d0ca01cb7f12a813e402919 (patch) | |
| tree | 121cbfde7f1b8334a9e9876481e9623567ce0f31 | |
| parent | d7611cb4c5613f807b2c9fb5efb61b7663fcc4bd (diff) | |
ajout Pnat (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/BinInt.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 42cb3675f5..e6257b243d 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -13,10 +13,10 @@ (***********************************************************) Require Export BinPos. +Require Export Pnat. Require BinNat. Require Plus. Require Mult. - (**********************************************************************) (** Binary integer numbers *) @@ -256,8 +256,6 @@ Qed. (**********************************************************************) (** Other properties of binary integer numbers *) -Hints Local Resolve compare_convert_O. - Lemma ZL0 : (S (S O))=(plus (S O) (S O)). Proof. Reflexivity. |