diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-23 18:17:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-23 18:17:38 +0000 |
| commit | c0f26dd0ebae4bad9a8850a198f0126ea4656e73 (patch) | |
| tree | 9e35faa7547ec7061d6c9b523b700046c7d80043 /theories/ZArith/Znumtheory.v | |
| parent | 582b5147cb79267ce79c03718cb3575826dc831c (diff) | |
Changement de précédence de l'argument du by de assert; conséquences sur les .v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 264c641ac..3a610226e 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -451,8 +451,7 @@ destruct a; intros; simpl; destruct (Zdiv_eucl b (Zpos p)) as (q,r); intros (H0,H1); rewrite inj_S in H; simpl Zabs in H; - (assert (H2: Zabs r < Z_of_nat n) by - rewrite Zabs_eq; auto with zarith); + assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith); assert (IH:=IHn r (Zpos p) H2); clear IHn; simpl in IH |- *; rewrite H0. @@ -527,7 +526,7 @@ destruct (Zle_lt_or_eq _ _ H2). generalize (IHn _ _ (conj H4 H3)). intros H5 H6 H7. replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. -assert (r = Zpos p * (-q) + b) by rewrite H1; ring. +assert (r = Zpos p * (-q) + b) by (rewrite H1; ring). destruct H5; auto. pattern r at 1; rewrite H8. apply Zis_gcd_sym. @@ -541,9 +540,9 @@ ring (Zpos p * 1); auto. apply Zmult_le_compat_l. destruct q. omega. -assert (0 < Zpos p0) by compute; auto. +assert (0 < Zpos p0) by (compute; auto). omega. -assert (Zpos p * Zneg p0 < 0) by compute; auto. +assert (Zpos p * Zneg p0 < 0) by (compute; auto). omega. compute; intros; discriminate. (* r=0 *) |