diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-05 15:42:40 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-05 15:42:40 +0000 |
| commit | c04fe01b5d33b5e091c8fd19047514a7e4c4f311 (patch) | |
| tree | 9ee176b3d4f6e432e6614fcc8b2570e187365cde /theories | |
| parent | 13aedc7b3ecd257ee83123d43ad06bd1e494635f (diff) | |
certains lemmes sont maintenant dans Rtrigo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2844 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 18 |
1 files changed, 1 insertions, 17 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 5b9422c59..dcadd84b8 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -369,20 +369,6 @@ Intro; Unfold sin; Replace ``(Rsqr (-x))`` with (Rsqr x); [Idtac | Apply Rsqr_ne Case (exist_sin (Rsqr x)); Intros; Ring. Qed. -(**********) -Axiom sin_plus : (x,y:R) ``(sin (x+y))==(sin x)*(cos y)+(cos x)*(sin y)``. -Axiom cos_plus : (x,y:R) ``(cos (x+y))==(cos x)*(cos y)-(sin x)*(sin y)``. - -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. -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. -Qed. - Lemma sin_0 : ``(sin 0)==0``. Unfold sin; Case (exist_sin (Rsqr R0)). Intros; Ring. @@ -414,6 +400,4 @@ Apply H0. Apply H. Exact (projT2 ? ? exist_cos0). Assert H := (projT2 ? ? (exist_cos (Rsqr R0))); Unfold cos; Pattern 1 R0; Replace R0 with (Rsqr R0); [Exact H | Apply Rsqr_O]. -Qed. - -Axiom sin_PI2 : ``(sin (PI/2))==1``. +Qed.
\ No newline at end of file |