diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-15 15:35:04 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-15 15:35:04 +0000 |
| commit | fea0a3265a7191a7e8c13028e7edd9bf29ba4d25 (patch) | |
| tree | f0993cfb172fd6e3cd280fcebf61ac0d6dc3e71b /theories/Reals/Rtrigo_alt.v | |
| parent | d72eb6e333f710bb8f4ea0061e8399aafba19fe0 (diff) | |
Nouvelle interprétation des nombres réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_alt.v')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 1cf745281..13ea21aa7 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -75,11 +75,12 @@ Apply Rsqr_incr_1. Apply Rle_trans with PI; [Assumption | Apply PI_4]. Assumption. Left; Sup0. -Pattern 1 ``16``; Rewrite <- Rplus_Or; Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring]. +Rewrite <- (Rplus_Or ``16``); Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring]. Rewrite <- (Rplus_sym ``20``); Pattern 1 ``20``; Rewrite <- Rplus_Or; Apply Rle_compatibility. Apply ge0_plus_ge0_is_ge0. Repeat Apply Rmult_le_pos. Left; Sup0. +Left; Sup0. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Apply Rmult_le_pos. @@ -214,6 +215,7 @@ Rewrite <- (Rplus_sym ``12``); Pattern 1 ``12``; Rewrite <- Rplus_Or; Apply Rle_ Apply ge0_plus_ge0_is_ge0. Repeat Apply Rmult_le_pos. Left; Sup0. +Left; Sup0. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Apply Rmult_le_pos. |