diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zdigits.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 043b68dd3..c658230d5 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -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. |