diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 07:25:23 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 07:25:23 +0000 |
| commit | d440c9c6b4c64bfea5e1dc6bc4003d677fd493ca (patch) | |
| tree | 19225b9e815613bf1cdf5982c4d9b09d9e1c51d7 /theories/Reals/Rlimit.v | |
| parent | 1a750105e7d9630acf44dd0833cdc34578a0aea5 (diff) | |
Field ne fait maintenant que les reductions necessaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 0c1ad9305..f31429d4a 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -618,8 +618,8 @@ Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*/(Rabsolu (f x))`` with ``(Rabsolu l)/2``. Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*(2*/(Rabsolu l))`` with ``(Rabsolu (f x))``. Assumption. -Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]]. -Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]]. +Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]]. +Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]]. Apply Rabsolu_no_R0; Assumption. Apply Rabsolu_no_R0; Assumption. Apply Rabsolu_no_R0; Assumption. @@ -631,7 +631,7 @@ Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rabsolu l)/2`` ``0`` H17 H15 Unfold Rdiv; Apply Rmult_lt_pos. Apply Rabsolu_pos_lt; Assumption. Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro; Assumption | Discriminate]. -Unfold Rdiv; Field; DiscrR. +Field; DiscrR. Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_r]]. Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_l]]. Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos. |