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/Zdiv.v | |
| parent | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (diff) | |
Testing a replacement of "cut" by "enough" on a couple of test files.
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 32993b2c0..f7843ea74 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -666,17 +666,15 @@ Theorem Zdiv_eucl_extended : {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}. Proof. intros b Hb a. - elim (Z_le_gt_dec 0 b); intro Hb'. - cut (b > 0); [ intro Hb'' | omega ]. - rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - cut (- b > 0); [ intro Hb'' | omega ]. - elim (Zdiv_eucl_exist Hb'' a); intros qr. - elim qr; intros q r Hqr. - exists (- q, r). - elim Hqr; intros. - split. - rewrite <- Z.mul_opp_comm; assumption. - rewrite Z.abs_neq; [ assumption | omega ]. + destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. + - assert (Hb'' : b > 0) by omega. + rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. + - assert (Hb'' : - b > 0) by omega. + destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). + exists (- q, r). + split. + + rewrite <- Z.mul_opp_comm; assumption. + + rewrite Z.abs_neq; [ assumption | omega ]. Qed. Arguments Zdiv_eucl_extended : default implicits. |