diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 14:03:27 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 14:03:27 +0000 |
| commit | ab6530c5a05cebc23dd677e251ac524bec6e8aee (patch) | |
| tree | 5c8e18d9e7cfc2debaac6f9ee4bb4c536c8f4da2 /theories/Reals/Rtrigo_calc.v | |
| parent | fb5304d62446fb2b054a6320e5368459f95b731f (diff) | |
Suppression de INR2 / Conséquence logique de la nouvelle représentation des constantes entières
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 3c87d0d50..004cbda0c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -386,8 +386,7 @@ Rewrite sqrt_def. Ring. Replace ``3`` with ``(INR (S (S (S O))))`` . Apply pos_INR. -Rewrite INR_eq_INR2. -Reflexivity. +Unfold INR; Rewrite Rplus_sym; Reflexivity. DiscrR. DiscrR. DiscrR. |