diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 07:25:23 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-17 07:25:23 +0000 |
| commit | d440c9c6b4c64bfea5e1dc6bc4003d677fd493ca (patch) | |
| tree | 19225b9e815613bf1cdf5982c4d9b09d9e1c51d7 /theories/Reals/Rtrigo.v | |
| parent | 1a750105e7d9630acf44dd0833cdc34578a0aea5 (diff) | |
Field ne fait maintenant que les reductions necessaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 1115ec19f..d1fc539f8 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -264,7 +264,7 @@ Intros; Elim (sin_eq_0 x); Intros; Apply (H1 H). Save. Lemma cos_eq_0_0 : (x:R) (cos x)==R0 -> (EXT k : Z | ``x==(IZR k)*PI+PI/2``). -Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Field; DiscrR. +Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Unfold INR; Field; DiscrR. Save. Lemma cos_eq_0_1 : (x:R) (EXT k : Z | ``x==(IZR k)*PI+PI/2``) -> ``(cos x)==0``. |