diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/ZArith/Zdigits.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/ZArith/Zdigits.v')
-rw-r--r-- | theories/ZArith/Zdigits.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index bf19c8ec..b5d04719 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,7 +41,7 @@ Section VALUE_OF_BOOLEAN_VECTORS. Lemma binary_value : forall n:nat, Bvector n -> Z. Proof. - simple induction n; intros. + refine (nat_rect _ _ _); intros. exact 0%Z. inversion H0. @@ -152,7 +152,7 @@ Section Z_BRIC_A_BRAC. Lemma binary_value_pos : forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. - induction bv as [| a n v IHbv]; simpl. + induction bv as [| a n v IHbv]; cbn. omega. destruct a; destruct (binary_value n v); simpl; auto. @@ -212,14 +212,11 @@ Section Z_BRIC_A_BRAC. (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros. - omega. - + enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega. rewrite <- two_power_nat_S. - destruct (Zeven.Zeven_odd_dec z); intros. + destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - - generalize (Zeven.Zodd_div2 z z0); omega. + generalize (Zeven.Zodd_div2 z Hodd); omega. Qed. Lemma Z_to_two_compl_Sn_z : |