diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
| commit | 3675bac6c38e0a26516e434be08bc100865b339b (patch) | |
| tree | 87f8eb1905c7b508dea60b1e216f79120e9e772d /theories/Reals/Rtrigo.v | |
| parent | c881bc37b91a201f7555ee021ccb74adb360d131 (diff) | |
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 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 60f07f610..6cba456fb 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1368,7 +1368,7 @@ intros; case (Rtotal_order x y); intro H4; Qed. (**********) -Lemma sin_eq_0_1 : forall x:R, ( exists k : Z | x = IZR k * PI) -> sin x = 0. +Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0. intros. elim H; intros. apply (Zcase_sign x0). @@ -1446,7 +1446,7 @@ rewrite Ropp_involutive. reflexivity. Qed. -Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z | x = IZR k * PI. +Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z, x = IZR k * PI. intros. assert (H0 := euclidian_division x PI PI_neq0). elim H0; intros q H1. @@ -1491,7 +1491,7 @@ exists q; reflexivity. Qed. Lemma cos_eq_0_0 : - forall x:R, cos x = 0 -> exists k : Z | x = IZR k * PI + PI / 2. + forall x:R, cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2. intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H); intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z; rewrite <- Z_R_minus; ring; rewrite Rmult_comm; rewrite <- H3; @@ -1500,7 +1500,7 @@ rewrite (double_var (- PI)); unfold Rdiv in |- *; ring. Qed. Lemma cos_eq_0_1 : - forall x:R, ( exists k : Z | x = IZR k * PI + PI / 2) -> cos x = 0. + forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0. intros x H1; rewrite cos_sin; elim H1; intros x0 H2; rewrite H2; replace (PI / 2 + (IZR x0 * PI + PI / 2)) with (IZR x0 * PI + PI). rewrite neg_sin; rewrite <- Ropp_0. |