diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
| commit | bcc5b59c086d1c06a1ec03ee0bff7647338bb258 (patch) | |
| tree | 4f332b460941cdbb211806659b1fe76253f2fc67 /theories/Reals/Exp_prop.v | |
| parent | 35cd1baf98895aa07d300d22c9e8148c91b43dac (diff) | |
Réorganisation de la librairie des réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Exp_prop.v')
| -rw-r--r-- | theories/Reals/Exp_prop.v | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 92f1e5293..ae6433466 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -8,15 +8,10 @@ (*i $Id$ i*) -Require Rbase. -Require DiscrR. -Require Rtrigo_fun. -Require Rseries. -Require Rtrigo_def. -Require Rtrigo_alt. -Require Cauchy_prod. -Require Binome. -Require Cos_plus. +Require RealsB. +Require Rfunctions. +Require SeqSeries. +Require Rtrigo. Require Ranalysis1. Require PSeries_reg. Require Div2. @@ -395,7 +390,7 @@ Rewrite <- mult_INR; Apply H1. Reflexivity. Left; Apply lt_INR_0; Apply H. Left; Apply Rmult_lt_pos. -Apply Rgt_2_0. +Sup0. Apply lt_INR_0; Apply div2_not_R0. Apply lt_n_S; Apply H. Cut (lt (1) (S N)). @@ -499,7 +494,7 @@ Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; R Symmetry ; Apply S_pred with O; Apply H7. Apply INR_lt. Apply Rlt_monotony_contra with (INR (2)). -Apply Rgt_2_0. +Simpl; Sup0. Rewrite Rmult_Or; Rewrite <- mult_INR. Apply lt_INR_0. Rewrite <- H6. @@ -529,7 +524,7 @@ Apply H2; Unfold ge. Cut (le (mult (2) (S N0)) n). Intro; Apply le_S_n. Apply INR_le; Apply Rle_monotony_contra with (INR (2)). -Apply Rgt_2_0. +Simpl; Sup0. Do 2 Rewrite <- mult_INR; Apply le_INR. Apply le_trans with n. Apply H4. @@ -552,7 +547,7 @@ Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; R Symmetry; Apply S_pred with O; Apply H8. Apply INR_lt. Apply Rlt_monotony_contra with (INR (2)). -Apply Rgt_2_0. +Simpl; Sup0. Rewrite Rmult_Or; Rewrite <- mult_INR. Apply lt_INR_0. Rewrite <- H7. |