diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-20 16:35:32 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-20 16:35:32 +0000 |
| commit | aa614e5692651ae621a0333ce947efd346a8e5d5 (patch) | |
| tree | c8e8a8856a48de66ee3f92a28d876b09df7e250e /theories/Reals/Rtrigo_calc.v | |
| parent | 3ba4abd9667cffb137e9b27e4b03e7229fcd56b4 (diff) | |
Cgt définition de plat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 0ecc9fbc5..3c87d0d50 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -471,7 +471,7 @@ Qed. (* Radian -> Degree | Degree -> Radian *) (***************************************************************) -Definition plat : R := (IZR `180`). +Definition plat : R := ``180``. Definition toRad [x:R] : R := ``x*PI*/plat``. Definition toDeg [x:R] : R := ``x*plat*/PI``. @@ -485,9 +485,7 @@ Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Rewrite <- Rinv_l_sym. Apply Rmult_1r. Apply PI_neq0. -Unfold plat. -Apply not_O_IZR. -Discriminate. +Unfold plat; DiscrR. Qed. Lemma toRad_inj : (x,y:R) (toRad x)==(toRad y) -> x==y. @@ -496,9 +494,7 @@ Rewrite <- (Rmult_sym x); Rewrite <- (Rmult_sym y). Apply r_Rmult_mult with ``/plat``. Rewrite <- (Rmult_sym ``x*PI``); Rewrite <- (Rmult_sym ``y*PI``); Assumption. Apply Rinv_neq_R0. -Unfold plat. -Apply not_O_IZR. -Discriminate. +Unfold plat; DiscrR. Apply PI_neq0. Qed. |