blob: 2d184fef1a897e4a0a6c9e072e8ab530eaed6069 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Rfunctions.
Require Import Fourier.
Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
intros; split_Rabs; fourier.
Qed.
Lemma l2 :
forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
intros.
split_Rabs; fourier.
Qed.
|
