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 (
Zabs 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, (
Zabs 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 Qle_Qabs :
forall a,
a <=
Qabs a.
Lemma Qabs_triangle_reverse :
forall x y,
Qabs x -
Qabs y <=
Qabs (
x -
y).