diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-03 18:26:47 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-03 18:26:47 +0000 |
| commit | bed9deeabad5e0935d55a37c0f2911d4d81ce84a (patch) | |
| tree | 07a3fa936d4dc71fb8ecb8e0898484e843b2a82e /theories/Reals/Rtrigo.v | |
| parent | 707990edb94cbb66abe025d32c2135bc517ef790 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 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 4a614bbf8..70452fbe0 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -25,7 +25,7 @@ Intros; Rewrite <- Ropp_mul1; Ring. Qed. (* Here, we have the euclidian division *) -(* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=2kPI *) +(* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *) Lemma euclidian_division : (x,y:R) ``y<>0`` -> (EXT k:Z | (EXT r : R | ``x==(IZR k)*y+r``/\``0<=r<(Rabsolu y)``)). Intros. Pose k0 := Cases (case_Rabsolu y) of |