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.