Library Coq.QArith.Qabs
Require Export QArith.
Require Export Qreduction.
#[
global]
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_Qlt_condition:
forall x y :
Q,
Qabs x < y <-> -y < x < y.
Lemma Qabs_diff_Qle_condition x y r:
Qabs (
x - y)
<= r <-> x - r <= y <= x + r.
Lemma Qabs_diff_Qlt_condition x y r:
Qabs (
x - y)
< r <-> x - r < y < x + r.
Lemma Qabs_ge:
forall r s :
Q,
r <= s -> r <= Qabs s.
Lemma Qabs_gt:
forall r s :
Q,
r < s -> r < Qabs s.