Library Coq.QArith.Qabs
Require Export QArith.
Require Export Qreduction.
Hint Resolve Qlt_le_weak :
qarith.
Definition Qabs (
x:
Q) :=
let (
n,
d):=
x in (
Z.abs n#d).
Lemma Qabs_case :
forall (
x:
Q) (
P :
Q -> Type),
(0
<= x -> P x) -> (x <= 0
-> P (
- x)
) -> P (
Qabs x).
Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd.
Qed.
Lemma Qabs_pos :
forall x, 0
<= x -> Qabs x == x.
Lemma Qabs_neg :
forall x,
x <= 0
-> Qabs x == - x.
Lemma Qabs_nonneg :
forall x, 0
<= (Qabs x).
Lemma Zabs_Qabs :
forall n d,
(Z.abs n#d)==Qabs (
n#d).
Lemma Qabs_opp :
forall x,
Qabs (
-x)
== Qabs x.
Lemma Qabs_triangle :
forall x y,
Qabs (
x+y)
<= Qabs x + Qabs y.
Lemma Qabs_Qmult :
forall a b,
Qabs (
a*b)
== (Qabs a)*(Qabs b).
Lemma Qabs_Qinv :
forall q,
Qabs (
/ q)
== / (Qabs q).
Lemma Qabs_Qminus x y:
Qabs (
x - y)
= Qabs (
y - x).
Lemma Qle_Qabs :
forall a,
a <= Qabs a.
Lemma Qabs_triangle_reverse :
forall x y,
Qabs x - Qabs y <= Qabs (
x - y).
Lemma Qabs_Qle_condition x y:
Qabs x <= y <-> -y <= x <= y.
Lemma Qabs_diff_Qle_condition x y r:
Qabs (
x - y)
<= r <-> x - r <= y <= x + r.