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.
|
