diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:30:04 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:30:04 +0000 |
| commit | 096310efb4266fe89455d473f704ec6c7ed5a97c (patch) | |
| tree | 17a6ed5acd135748f43ecb944e268657731a55a2 /theories/Reals/Rtrigo.v | |
| parent | cb7cf50289fbf1c5fe60fd915f63128c88dc6d68 (diff) | |
Renommages dans Rtrigo_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 631757abe..8210b35f1 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -31,7 +31,7 @@ Qed. (**********) Lemma cos_minus : (x,y:R) ``(cos (x-y))==(cos x)*(cos y)+(sin x)*(sin y)``. Intros; Unfold Rminus; Rewrite cos_plus. -Rewrite <- cos_paire; Rewrite sin_impaire; Ring. +Rewrite <- cos_sym; Rewrite sin_antisym; Ring. Qed. (**********) @@ -94,7 +94,7 @@ Qed. Lemma sin_minus : (x,y:R) ``(sin (x-y))==(sin x)*(cos y)-(cos x)*(sin y)``. Intros; Unfold Rminus; Rewrite sin_plus. -Rewrite <- cos_paire; Rewrite sin_impaire; Ring. +Rewrite <- cos_sym; Rewrite sin_antisym; Ring. Qed. (**********) @@ -151,11 +151,11 @@ Repeat Rewrite double; Intros; Repeat Rewrite double; Rewrite double in H0; Appl Qed. Lemma sin_neg : (x:R) ``(sin (-x))==-(sin x)``. -Apply sin_impaire. +Apply sin_antisym. Qed. Lemma cos_neg : (x:R) ``(cos (-x))==(cos x)``. -Intro; Symmetry; Apply cos_paire. +Intro; Symmetry; Apply cos_sym. Qed. Lemma tan_0 : ``(tan 0)==0``. |