diff options
| -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. |