aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo_reg.v
diff options
context:
space:
mode:
authorGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-15 15:30:59 +0000
committerGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-15 15:30:59 +0000
commit99f4c55d9b9eb1130bff54a1ff9028b442141231 (patch)
treea996b35f7fb7ab35dd616a4b2a162948b9e550be /theories/Reals/Rtrigo_reg.v
parent1029596ed3c5b86162f4a4717fe2e50df70cb837 (diff)
Changement dans ring et field, beaucoup de correction d'erreurs,
maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_reg.v')
-rw-r--r--theories/Reals/Rtrigo_reg.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index ba1716506..9b5111ff9 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -99,7 +99,7 @@ Proof.
apply pow_nonzero; assumption.
replace (2 * S n)%nat with (S (S (2 * n))).
simpl in |- *; ring.
- ring_nat.
+ ring.
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
apply pow_nonzero; assumption.
replace (2 * S n)%nat with (S (S (2 * n))).
simpl in |- *; ring.
- ring_nat.
+ ring.
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rabs_no_R0; apply pow_nonzero; assumption.