blob: e522cb74f098afa18f5afaa95ac132486f5ad20c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require SplitAbsolu.
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.
|
