diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 13:11:19 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 13:11:19 +0000 |
| commit | d5ab2a4d38a38db278a78e67d762c052b8e8e606 (patch) | |
| tree | b98ecec33e2d08f4ce78ed2ec04e6899972bbdb2 /theories/Reals/Cos_rel.v | |
| parent | 314333e2ce7c06293ab6e5292b2927afb75b6a6f (diff) | |
Renommages dans PartSum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Cos_rel.v')
| -rw-r--r-- | theories/Reals/Cos_rel.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index f1675e8d5..f1275c3db 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -271,7 +271,7 @@ Case (exist_cos (Rsqr x)). Unfold Rsqr; Intros. Unfold cos_in in p_i. Unfold cos_in in c. -Apply unicite_sum with [i:nat]``(cos_n i)*(pow (x*x) i)``; Assumption. +Apply unicity_sum with [i:nat]``(cos_n i)*(pow (x*x) i)``; Assumption. Qed. Lemma C1_cvg : (x,y:R) (Un_cv (C1 x y) (cos (Rplus x y))). @@ -301,7 +301,7 @@ Case (exist_cos (Rsqr ``x+y``)). Unfold Rsqr; Intros. Unfold cos_in in p_i. Unfold cos_in in c. -Apply unicite_sum with [i:nat]``(cos_n i)*(pow ((x+y)*(x+y)) i)``; Assumption. +Apply unicity_sum with [i:nat]``(cos_n i)*(pow ((x+y)*(x+y)) i)``; Assumption. Qed. Lemma B1_cvg : (x:R) (Un_cv (B1 x) (sin x)). @@ -353,6 +353,6 @@ Case (exist_sin (Rsqr x)). Unfold Rsqr; Intros. Unfold sin_in in p_i. Unfold sin_in in s. -Assert H1 := (unicite_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). +Assert H1 := (unicity_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). Rewrite H1; Reflexivity. Qed. |