diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-02 18:53:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:21 +0200 |
| commit | 8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (patch) | |
| tree | 77db789ac60664e7eeb2e1b078a32e8f7879384b /theories/ZArith/Zdigits.v | |
| parent | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (diff) | |
Testing a replacement of "cut" by "enough" on a couple of test files.
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. |