diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 15:45:22 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-21 15:45:22 +0000 |
| commit | 785771ebd3f16778712828bee0aba79bb01e6525 (patch) | |
| tree | dcbe71b242f651c33a422e1e163d1047219d7dbe /theories/Reals/Rtrigo_def.v | |
| parent | ebb7b5514582369bc241f71ab811fa152b9d0e37 (diff) | |
Renommage dans Alembert.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3557 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 9d09f1a53..fdeefb6f3 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -26,7 +26,7 @@ Apply INR_fact_neq_0. Qed. Lemma exist_exp : (x:R)(SigT R [l:R](exp_in x l)). -Intro; Generalize (Alembert [n:nat](Rinv (INR (fact n))) x exp_cof_no_R0 Alembert_exp). +Intro; Generalize (Alembert_C3 [n:nat](Rinv (INR (fact n))) x exp_cof_no_R0 Alembert_exp). Unfold Pser exp_in. Trivial. Defined. @@ -203,7 +203,7 @@ Definition cos_in:R->R->Prop := [x,l:R](infinit_sum [i:nat]``(cos_n i)*(pow x i) (**********) Lemma exist_cos : (x:R)(SigT R [l:R](cos_in x l)). -Intro; Generalize (Alembert cos_n x cosn_no_R0 Alembert_cos). +Intro; Generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos). Unfold Pser cos_in; Trivial. Qed. @@ -301,7 +301,7 @@ Definition sin_in:R->R->Prop := [x,l:R](infinit_sum [i:nat]``(sin_n i)*(pow x i) (**********) Lemma exist_sin : (x:R)(SigT R [l:R](sin_in x l)). -Intro; Generalize (Alembert sin_n x sin_no_R0 Alembert_sin). +Intro; Generalize (Alembert_C3 sin_n x sin_no_R0 Alembert_sin). Unfold Pser sin_n; Trivial. Qed. |