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/Rtrigo_def.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/Rtrigo_def.v')
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index fdeefb6f3..038f1efb7 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -57,7 +57,7 @@ Defined. Lemma exp_0 : ``(exp 0)==1``. Cut (exp_in R0 (exp R0)). Cut (exp_in R0 R1). -Unfold exp_in; Intros; EApply unicite_sum. +Unfold exp_in; Intros; EApply unicity_sum. Apply H0. Apply H. Exact (projT2 ? ? exist_exp0). @@ -350,7 +350,7 @@ Defined. Lemma cos_0 : ``(cos 0)==1``. Cut (cos_in R0 (cos R0)). Cut (cos_in R0 R1). -Unfold cos_in; Intros; EApply unicite_sum. +Unfold cos_in; Intros; EApply unicity_sum. Apply H0. Apply H. Exact (projT2 ? ? exist_cos0). |