diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-12 17:15:22 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-12 17:15:22 +0000 |
| commit | cae62c87e2a361aeb31d3382280e5d7f18126e92 (patch) | |
| tree | 4bca5f02028b68e98db4e34127f1e738dbc6d5b9 /theories/ZArith/Zdiv.v | |
| parent | bb3218e21e82cadacc2e22d9b55e3033df1744bb (diff) | |
normalisation (by closure) was not performed under fixpoints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index d168b0369..f9601b09a 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Contribution by Claude Marché and Xavier Urbain *) +(* Contribution by Claude Marché and Xavier Urbain *) (** Euclidean Division @@ -129,7 +129,8 @@ Lemma Z_div_mod_POS : forall a:positive, let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. Proof. -simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. +simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *; + fold Zdiv_eucl_POS in |- *; cbv zeta. intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. generalize (Zgt_cases b (2 * r + 1)). @@ -238,7 +239,8 @@ Qed. Lemma Z_div_POS_ge0 : forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0. Proof. - simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. + simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *; + fold Zdiv_eucl_POS in |- *; cbv zeta. intro p; case (Zdiv_eucl_POS p b). intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega. intro p; case (Zdiv_eucl_POS p b). |