diff options
Diffstat (limited to 'theories/ZArith/Zdigits.v')
| -rw-r--r-- | theories/ZArith/Zdigits.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index e5325aa75..043b68dd3 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -212,13 +212,10 @@ 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) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z Hodd); omega. Qed. |