diff options
Diffstat (limited to 'test-suite/success/Fourier.v')
| -rw-r--r-- | test-suite/success/Fourier.v | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v index f1f7ae080..2d184fef1 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/Fourier.v @@ -1,16 +1,12 @@ -Require Rfunctions. -Require Fourier. +Require Import Rfunctions. +Require Import Fourier. -Lemma l1: - (x, y, z : R) - ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``. -Intros; SplitAbsolu; Fourier. +Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). +intros; split_Rabs; fourier. Qed. -Lemma l2: - (x, y : R) - ``x < (Rabsolu y)`` -> - ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` -> ``(Rabsolu x) <= 1``. -Intros. -SplitAbsolu; Fourier. +Lemma l2 : + forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. +intros. +split_Rabs; fourier. Qed. |