aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Fourier.v
blob: f1f7ae080b45ec57193407c530ca212703767890 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Require Rfunctions.
Require Fourier.
 
Lemma l1:
 (x, y, z : R)
  ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``.
Intros; SplitAbsolu; Fourier.
Qed.
 
Lemma l2:
 (x, y : R)
 ``x < (Rabsolu y)`` ->
 ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` ->  ``(Rabsolu x) <= 1``.
Intros.
SplitAbsolu; Fourier.
Qed.