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