diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-02 12:46:14 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-02 12:46:14 +0000 |
| commit | fbf316e4e862704b4ad82255c34592b701507742 (patch) | |
| tree | 584fd2ddf37f0292f6eed0c6c827ca7138904264 /theories/Reals/Rbase.v | |
| parent | 0ff1ec3668b036f14159f97c25008f3570513147 (diff) | |
Optimisation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2582 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rbase.v')
| -rw-r--r-- | theories/Reals/Rbase.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index ca1853405..f20254f62 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1549,7 +1549,20 @@ Rewrite Rmult_1r; Replace ``2*x`` with ``x+x``. Rewrite (Rplus_sym y); Intro H5; Apply Rle_anti_compatibility with x; Assumption. Ring. Replace ``2`` with (INR (S (S O))); [Apply not_O_INR; Discriminate | Ring]. -Field; Replace ``2`` with (INR (S (S O))); [Apply not_O_INR; Discriminate | Ring]. +Pattern 2 y; Replace y with ``y/2+y/2``. +Unfold Rminus Rdiv. +Repeat Rewrite Rmult_Rplus_distrl. +Ring. +Cut (z:R) ``2*z == z + z``. +Intro. +Rewrite <- (H4 ``y/2``). +Unfold Rdiv. +Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. +Replace ``2`` with (INR (2)). +Apply not_O_INR. +Discriminate. +Unfold INR; Reflexivity. +Intro; Ring. Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro; Assumption | Discriminate]. Save. |