Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export ZArith.
Require Export ZArithRing.
Require Export Morphisms Setoid Bool.

Definition of Q and basic properties

Rationals are pairs of Z and positive numbers.

Record Q : Set := Qmake {Qnum : Z; Qden : positive}.

Declare Scope Q_scope.
Delimit Scope Q_scope with Q.
Bind Scope Q_scope with Q.
Arguments Qmake _%Z _%positive.
Open Scope Q_scope.
Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.

a#b denotes the fraction a over b.

Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.

Definition of_decimal (d:Decimal.decimal) : Q :=
  let '(i, f, e) :=
    match d with
    | Decimal.Decimal i f => (i, f, Decimal.Pos Decimal.Nil)
    | Decimal.DecimalExp i f e => (i, f, e)
    end in
  let num := Z.of_int (Decimal.app_int i f) in
  let e := Z.sub (Z.of_int e) (Z.of_nat (Decimal.nb_digits f)) in
  match e with
  | Z0 => Qmake num 1
  | Zpos e => Qmake (Pos.iter (Z.mul 10) num e) 1
  | Zneg e => Qmake num (Pos.iter (Pos.mul 10) 1%positive e)
  end.

Definition to_decimal (q:Q) : option Decimal.decimal :=
  let num := Z.to_int (Qnum q) in
  let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
  match den with
  | Decimal.D1 Decimal.Nil =>
    match Z.of_nat e_den with
    | Z0 => Some (Decimal.Decimal num Decimal.Nil)
    | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e)))
    end
  | _ => None
  end.

Numeral Notation Q of_decimal to_decimal : Q_scope.

Definition inject_Z (x : Z) := Qmake x 1.
Arguments inject_Z x%Z.

Notation QDen p := (Zpos (Qden p)).

Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z.
Notation Qgt a b := (Qlt b a) (only parsing).
Notation Qge a b := (Qle b a) (only parsing).

Infix "==" := Qeq (at level 70, no associativity) : Q_scope.
Infix "<" := Qlt : Q_scope.
Infix "<=" := Qle : Q_scope.
Notation "x > y" := (Qlt y x)(only parsing) : Q_scope.
Notation "x >= y" := (Qle y x)(only parsing) : Q_scope.
Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.

injection from Z is injective.

Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.a, b:Z
inject_Z a == inject_Z b <-> a = b
Proof.a, b:Z
inject_Z a == inject_Z b <-> a = b
 unfold Qeq.a, b:Z
(Qnum (inject_Z a) * QDen (inject_Z b))%Z =
(Qnum (inject_Z b) * QDen (inject_Z a))%Z <-> a = b simpl.a, b:Z
(a * 1)%Z = (b * 1)%Z <-> a = b omega.
Qed.

Another approach : using Qcompare for defining order relations.

Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z.
Notation "p ?= q" := (Qcompare p q) : Q_scope.

Lemma Qeq_alt p q : (p == q) <-> (p ?= q) = Eq.p, q:Q
p == q <-> (p ?= q) = Eq
Proof.p, q:Q
p == q <-> (p ?= q) = Eq
symmetry.p, q:Q
(p ?= q) = Eq <-> p == q apply Z.compare_eq_iff.
Qed.

Lemma Qlt_alt p q : (p<q) <-> (p?=q = Lt).p, q:Q
p < q <-> (p ?= q) = Lt
Proof.p, q:Q
p < q <-> (p ?= q) = Lt
reflexivity.
Qed.

Lemma Qgt_alt p q : (p>q) <-> (p?=q = Gt).p, q:Q
q < p <-> (p ?= q) = Gt
Proof.p, q:Q
q < p <-> (p ?= q) = Gt
symmetry.p, q:Q
(p ?= q) = Gt <-> q < p apply Z.gt_lt_iff.
Qed.

Lemma Qle_alt p q : (p<=q) <-> (p?=q <> Gt).p, q:Q
p <= q <-> (p ?= q) <> Gt
Proof.p, q:Q
p <= q <-> (p ?= q) <> Gt
reflexivity.
Qed.

Lemma Qge_alt p q : (p>=q) <-> (p?=q <> Lt).p, q:Q
q <= p <-> (p ?= q) <> Lt
Proof.p, q:Q
q <= p <-> (p ?= q) <> Lt
symmetry.p, q:Q
(p ?= q) <> Lt <-> q <= p apply Z.ge_le_iff.
Qed.

Hint Unfold Qeq Qlt Qle : qarith.
Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.

Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x).x, y:Q
CompOpp (x ?= y) = (y ?= x)
Proof.x, y:Q
CompOpp (x ?= y) = (y ?= x)
 symmetry.x, y:Q
(y ?= x) = CompOpp (x ?= y) apply Z.compare_antisym.
Qed.

Lemma Qcompare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x ?= y).x, y:Q
CompareSpec (x == y) (x < y) (y < x) (x ?= y)
Proof.x, y:Q
CompareSpec (x == y) (x < y) (y < x) (x ?= y)
 unfold Qeq, Qlt, Qcompare.x, y:Q
CompareSpec
  ((Qnum x * QDen y)%Z = (Qnum y * QDen x)%Z)
  (Qnum x * QDen y < Qnum y * QDen x)%Z
  (Qnum y * QDen x < Qnum x * QDen y)%Z
  (Qnum x * QDen y ?= Qnum y * QDen x)%Z case Z.compare_spec; now constructor.
Qed.

Properties of equality.

Theorem Qeq_refl x : x == x.x:Q
x == x
Proof.x:Q
x == x
 auto with qarith.
Qed.

Theorem Qeq_sym x y : x == y -> y == x.x, y:Q
x == y -> y == x
Proof.x, y:Q
x == y -> y == x
 auto with qarith.
Qed.

Theorem Qeq_trans x y z : x == y -> y == z -> x == z.x, y, z:Q
x == y -> y == z -> x == z
Proof.x, y, z:Q
x == y -> y == z -> x == z
unfold Qeq; intros XY YZ.x, y, z:Q
XY:(Qnum x * QDen y)%Z = (Qnum y * QDen x)%Z
YZ:(Qnum y * QDen z)%Z = (Qnum z * QDen y)%Z
(Qnum x * QDen z)%Z = (Qnum z * QDen x)%Z
apply Z.mul_reg_r with (QDen y); [auto with qarith|].x, y, z:Q
XY:(Qnum x * QDen y)%Z = (Qnum y * QDen x)%Z
YZ:(Qnum y * QDen z)%Z = (Qnum z * QDen y)%Z
(Qnum x * QDen z * QDen y)%Z =
(Qnum z * QDen x * QDen y)%Z
now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0.
Qed.

Hint Immediate Qeq_sym : qarith.
Hint Resolve Qeq_refl Qeq_trans : qarith.

In a word, Qeq is a setoid equality.

Instance Q_Setoid : Equivalence Qeq.Equivalence Qeq
Proof.Equivalence Qeq split; red; eauto with qarith. Qed.

Furthermore, this equality is decidable:

Theorem Qeq_dec x y : {x==y} + {~ x==y}.x, y:Q
{x == y} + {~ x == y}
Proof.x, y:Q
{x == y} + {~ x == y}
 apply Z.eq_dec.
Defined.

Definition Qeq_bool x y :=
  (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.

Definition Qle_bool x y :=
  (Z.leb (Qnum x * QDen y) (Qnum y * QDen x))%Z.

Lemma Qeq_bool_iff x y : Qeq_bool x y = true <-> x == y.x, y:Q
Qeq_bool x y = true <-> x == y
Proof.x, y:Q
Qeq_bool x y = true <-> x == y
  symmetry; apply Zeq_is_eq_bool.
Qed.

Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y.x, y:Q
Qeq_bool x y = true -> x == y
Proof.x, y:Q
Qeq_bool x y = true -> x == y
  apply Qeq_bool_iff.
Qed.

Lemma Qeq_eq_bool x y : x == y -> Qeq_bool x y = true.x, y:Q
x == y -> Qeq_bool x y = true
Proof.x, y:Q
x == y -> Qeq_bool x y = true
  apply Qeq_bool_iff.
Qed.

Lemma Qeq_bool_neq x y : Qeq_bool x y = false -> ~ x == y.x, y:Q
Qeq_bool x y = false -> ~ x == y
Proof.x, y:Q
Qeq_bool x y = false -> ~ x == y
  rewrite <- Qeq_bool_iff.x, y:Q
Qeq_bool x y = false -> Qeq_bool x y <> true now intros ->.
Qed.

Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y.x, y:Q
Qle_bool x y = true <-> x <= y
Proof.x, y:Q
Qle_bool x y = true <-> x <= y
  symmetry; apply Zle_is_le_bool.
Qed.

Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y.x, y:Q
Qle_bool x y = true -> x <= y
Proof.x, y:Q
Qle_bool x y = true -> x <= y
  apply Qle_bool_iff.
Qed.

Theorem Qnot_eq_sym x y : ~x == y -> ~y == x.x, y:Q
~ x == y -> ~ y == x
Proof.x, y:Q
~ x == y -> ~ y == x
 auto with qarith.
Qed.

Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.x, y:Q
Qeq_bool x y = Qeq_bool y x
Proof.x, y:Q
Qeq_bool x y = Qeq_bool y x
 apply eq_true_iff_eq.x, y:Q
Qeq_bool x y = true <-> Qeq_bool y x = true rewrite !Qeq_bool_iff.x, y:Q
x == y <-> y == x now symmetry.
Qed.

Lemma Qeq_bool_refl x: Qeq_bool x x = true.x:Q
Qeq_bool x x = true
Proof.x:Q
Qeq_bool x x = true
  rewrite Qeq_bool_iff.x:Q
x == x now reflexivity.
Qed.

Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.x, y:Q
Qeq_bool x y = true -> Qeq_bool y x = true
Proof.x, y:Q
Qeq_bool x y = true -> Qeq_bool y x = true
  rewrite !Qeq_bool_iff.x, y:Q
x == y -> y == x now symmetry.
Qed.

Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.x, y, z:Q
Qeq_bool x y = true ->
Qeq_bool y z = true -> Qeq_bool x z = true
Proof.x, y, z:Q
Qeq_bool x y = true ->
Qeq_bool y z = true -> Qeq_bool x z = true
  rewrite !Qeq_bool_iff; apply Qeq_trans.
Qed.

Hint Resolve Qnot_eq_sym : qarith.

Addition, multiplication and opposite

The addition, multiplication and opposite are defined in the straightforward way:

Definition Qplus (x y : Q) :=
  (Qnum x * QDen y + Qnum y * QDen x) # (Qden x * Qden y).

Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y).

Definition Qopp (x : Q) := (- Qnum x) # (Qden x).

Definition Qminus (x y : Q) := Qplus x (Qopp y).

Definition Qinv (x : Q) :=
  match Qnum x with
  | Z0 => 0
  | Zpos p => (QDen x)#p
  | Zneg p => (Zneg (Qden x))#p
  end.

Definition Qdiv (x y : Q) := Qmult x (Qinv y).

Infix "+" := Qplus : Q_scope.
Notation "- x" := (Qopp x) : Q_scope.
Infix "-" := Qminus : Q_scope.
Infix "*" := Qmult : Q_scope.
Notation "/ x" := (Qinv x) : Q_scope.
Infix "/" := Qdiv : Q_scope.

A light notation for Zpos

Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).a:Z
b:positive
a # b == inject_Z a / inject_Z (Z.pos b)
Proof.a:Z
b:positive
a # b == inject_Z a / inject_Z (Z.pos b)
unfold Qeq.a:Z
b:positive
(Qnum (a # b) * QDen (inject_Z a / inject_Z (Z.pos b)))%Z =
(Qnum (inject_Z a / inject_Z (Z.pos b)) * QDen (a # b))%Z simpl.a:Z
b:positive
(a * Z.pos b)%Z = (a * 1 * Z.pos b)%Z ring.
Qed.

Setoid compatibility results

Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus.Proper (Qeq ==> Qeq ==> Qeq) Qplus
Proof.Proper (Qeq ==> Qeq ==> Qeq) Qplus
  unfold Qeq, Qplus; simpl.Proper
  ((fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z))
  (fun x y : Q =>
   Qnum x * QDen y + Qnum y * QDen x # Qden x * Qden y)
  Open Scope Z_scope.Proper
  ((fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p))
  (fun x y : Q =>
   Qnum x * QDen y + Qnum y * QDen x # Qden x * Qden y)
  intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
(p1 * Z.pos r2 + r1 * Z.pos p2) * Z.pos (q2 * s2) =
(q1 * Z.pos s2 + s1 * Z.pos q2) * Z.pos (p2 * r2)
  simpl_mult; ring_simplify.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * Z.pos r2 * Z.pos q2 * Z.pos s2 +
r1 * Z.pos p2 * Z.pos q2 * Z.pos s2 =
Z.pos r2 * Z.pos p2 * Z.pos q2 * s1 +
Z.pos r2 * Z.pos p2 * Z.pos s2 * q1
  replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * Z.pos q2 * Z.pos r2 * Z.pos s2 +
r1 * Z.pos p2 * Z.pos q2 * Z.pos s2 =
Z.pos r2 * Z.pos p2 * Z.pos q2 * s1 +
Z.pos r2 * Z.pos p2 * Z.pos s2 * q1
  rewrite H.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
q1 * Z.pos p2 * Z.pos r2 * Z.pos s2 +
r1 * Z.pos p2 * Z.pos q2 * Z.pos s2 =
Z.pos r2 * Z.pos p2 * Z.pos q2 * s1 +
Z.pos r2 * Z.pos p2 * Z.pos s2 * q1
  replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
q1 * Z.pos p2 * Z.pos r2 * Z.pos s2 +
r1 * Z.pos s2 * Z.pos p2 * Z.pos q2 =
Z.pos r2 * Z.pos p2 * Z.pos q2 * s1 +
Z.pos r2 * Z.pos p2 * Z.pos s2 * q1
  rewrite H0.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
q1 * Z.pos p2 * Z.pos r2 * Z.pos s2 +
s1 * Z.pos r2 * Z.pos p2 * Z.pos q2 =
Z.pos r2 * Z.pos p2 * Z.pos q2 * s1 +
Z.pos r2 * Z.pos p2 * Z.pos s2 * q1
  ring.
  Close Scope Z_scope.
Qed.

Instance Qopp_comp : Proper (Qeq==>Qeq) Qopp.Proper (Qeq ==> Qeq) Qopp
Proof.Proper (Qeq ==> Qeq) Qopp
  unfold Qeq, Qopp; simpl.Proper
  ((fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z))
  (fun x : Q => - Qnum x # Qden x)
  Open Scope Z_scope.Proper
  ((fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p))
  (fun x : Q => - Qnum x # Qden x)
  intros x y H; simpl.x, y:Q
H:Qnum x * QDen y = Qnum y * QDen x
- Qnum x * QDen y = - Qnum y * QDen x
  replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring.x, y:Q
H:Qnum x * QDen y = Qnum y * QDen x
- (Qnum x * QDen y) = - Qnum y * QDen x
  rewrite H;  ring.
  Close Scope Z_scope.
Qed.

Instance Qminus_comp : Proper (Qeq==>Qeq==>Qeq) Qminus.Proper (Qeq ==> Qeq ==> Qeq) Qminus
Proof.Proper (Qeq ==> Qeq ==> Qeq) Qminus
  intros x x' Hx y y' Hy.x, x':Q
Hx:x == x'
y, y':Q
Hy:y == y'
x - y == x' - y'
  unfold Qminus.x, x':Q
Hx:x == x'
y, y':Q
Hy:y == y'
x + - y == x' + - y' rewrite Hx, Hy; auto with qarith.
Qed.

Instance Qmult_comp : Proper (Qeq==>Qeq==>Qeq) Qmult.Proper (Qeq ==> Qeq ==> Qeq) Qmult
Proof.Proper (Qeq ==> Qeq ==> Qeq) Qmult
  unfold Qeq; simpl.Proper
  ((fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z)) Qmult
  Open Scope Z_scope.Proper
  ((fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p))
  Qmult
  intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * r1 * Z.pos (q2 * s2) = q1 * s1 * Z.pos (p2 * r2)
  intros; simpl_mult; ring_simplify.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * r1 * Z.pos q2 * Z.pos s2 =
q1 * s1 * Z.pos p2 * Z.pos r2
  replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * r1 * Z.pos q2 * Z.pos s2 =
q1 * Z.pos p2 * s1 * Z.pos r2
  rewrite <- H.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
p1 * r1 * Z.pos q2 * Z.pos s2 =
p1 * Z.pos q2 * s1 * Z.pos r2
  replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
r1 * Z.pos s2 * p1 * Z.pos q2 =
p1 * Z.pos q2 * s1 * Z.pos r2
  rewrite H0.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H0:r1 * Z.pos s2 = s1 * Z.pos r2
s1 * Z.pos r2 * p1 * Z.pos q2 =
p1 * Z.pos q2 * s1 * Z.pos r2
  ring.
  Close Scope Z_scope.
Qed.

Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv.Proper (Qeq ==> Qeq) Qinv
Proof.Proper (Qeq ==> Qeq) Qinv
  unfold Qeq, Qinv; simpl.Proper
  ((fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z))
  (fun x : Q =>
   match Qnum x with
   | 0%Z => 0
   | Z.pos p => QDen x # p
   | Z.neg p => Z.neg (Qden x) # p
   end)
  Open Scope Z_scope.Proper
  ((fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p))
  (fun x : Q =>
   match Qnum x with
   | 0 => 0%Q
   | Z.pos p => QDen x # p
   | Z.neg p => Z.neg (Qden x) # p
   end)
  intros (p1, p2) (q1, q2) EQ; simpl in *.p1:Z
p2:positive
q1:Z
q2:positive
EQ:p1 * Z.pos q2 = q1 * Z.pos p2
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p => Z.pos p2 # p
  | Z.neg p => Z.neg p2 # p
  end *
QDen
  match q1 with
  | 0%Z => 0
  | Z.pos p => Z.pos q2 # p
  | Z.neg p => Z.neg q2 # p
  end =
Qnum
  match q1 with
  | 0%Z => 0
  | Z.pos p => Z.pos q2 # p
  | Z.neg p => Z.neg q2 # p
  end *
QDen
  match p1 with
  | 0%Z => 0
  | Z.pos p => Z.pos p2 # p
  | Z.neg p => Z.neg p2 # p
  end
  destruct q1; simpl in *.p1:Z
p2, q2:positive
EQ:p1 * Z.pos q2 = 0
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p => Z.pos p2 # p
  | Z.neg p => Z.neg p2 # p
  end * 1 = 0
p1:Z
p2, p, q2:positive
EQ:p1 * Z.pos q2 = Z.pos (p * p2)
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p0 => Z.pos p2 # p0
  | Z.neg p0 => Z.neg p2 # p0
  end * Z.pos p =
Z.pos
  (q2 *
   Qden
     match p1 with
     | 0%Z => 0
     | Z.pos p0 => Z.pos p2 # p0
     | Z.neg p0 => Z.neg p2 # p0
     end)
p1:Z
p2, p, q2:positive
EQ:p1 * Z.pos q2 = Z.neg (p * p2)
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p0 => Z.pos p2 # p0
  | Z.neg p0 => Z.neg p2 # p0
  end * Z.pos p =
Z.neg
  (q2 *
   Qden
     match p1 with
     | 0%Z => 0
     | Z.pos p0 => Z.pos p2 # p0
     | Z.neg p0 => Z.neg p2 # p0
     end)
  -p1:Z
p2, q2:positive
EQ:p1 * Z.pos q2 = 0
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p => Z.pos p2 # p
  | Z.neg p => Z.neg p2 # p
  end * 1 = 0 apply Z.mul_eq_0 in EQ.p1:Z
p2, q2:positive
EQ:p1 = 0 \/ Z.pos q2 = 0
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p => Z.pos p2 # p
  | Z.neg p => Z.neg p2 # p
  end * 1 = 0 destruct EQ; now subst.
  -p1:Z
p2, p, q2:positive
EQ:p1 * Z.pos q2 = Z.pos (p * p2)
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p0 => Z.pos p2 # p0
  | Z.neg p0 => Z.neg p2 # p0
  end * Z.pos p =
Z.pos
  (q2 *
   Qden
     match p1 with
     | 0%Z => 0
     | Z.pos p0 => Z.pos p2 # p0
     | Z.neg p0 => Z.neg p2 # p0
     end) destruct p1; simpl in *; try discriminate.p0, p2, p, q2:positive
EQ:Z.pos (p0 * q2) = Z.pos (p * p2)
Z.pos (p2 * p) = Z.pos (q2 * p0)
    now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm.
  -p1:Z
p2, p, q2:positive
EQ:p1 * Z.pos q2 = Z.neg (p * p2)
Qnum
  match p1 with
  | 0%Z => 0
  | Z.pos p0 => Z.pos p2 # p0
  | Z.neg p0 => Z.neg p2 # p0
  end * Z.pos p =
Z.neg
  (q2 *
   Qden
     match p1 with
     | 0%Z => 0
     | Z.pos p0 => Z.pos p2 # p0
     | Z.neg p0 => Z.neg p2 # p0
     end) destruct p1; simpl in *; try discriminate.p0, p2, p, q2:positive
EQ:Z.neg (p0 * q2) = Z.neg (p * p2)
Z.neg (p2 * p) = Z.neg (q2 * p0)
    now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm.
  Close Scope Z_scope.
Qed.

Instance Qdiv_comp : Proper (Qeq==>Qeq==>Qeq) Qdiv.Proper (Qeq ==> Qeq ==> Qeq) Qdiv
Proof.Proper (Qeq ==> Qeq ==> Qeq) Qdiv
  intros x x' Hx y y' Hy; unfold Qdiv.x, x':Q
Hx:x == x'
y, y':Q
Hy:y == y'
x * / y == x' * / y'
  rewrite Hx, Hy; auto with qarith.
Qed.

Instance Qcompare_comp : Proper (Qeq==>Qeq==>eq) Qcompare.Proper (Qeq ==> Qeq ==> eq) Qcompare
Proof.Proper (Qeq ==> Qeq ==> eq) Qcompare
  unfold Qeq, Qcompare.Proper
  ((fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==>
   (fun p q : Q =>
    (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z) ==> eq)
  (fun p q : Q =>
   (Qnum p * QDen q ?= Qnum q * QDen p)%Z)
  Open Scope Z_scope.Proper
  ((fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   (fun p q : Q => Qnum p * QDen q = Qnum q * QDen p) ==>
   eq)
  (fun p q : Q => Qnum p * QDen q ?= Qnum q * QDen p)
  intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(p1 * Z.pos r2 ?= r1 * Z.pos p2) =
(q1 * Z.pos s2 ?= s1 * Z.pos q2)
  rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)).p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(Z.pos (q2 * s2) * (p1 * Z.pos r2)
 ?= Z.pos (q2 * s2) * (r1 * Z.pos p2)) =
(q1 * Z.pos s2 ?= s1 * Z.pos q2)
  rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)).p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(Z.pos (q2 * s2) * (p1 * Z.pos r2)
 ?= Z.pos (q2 * s2) * (r1 * Z.pos p2)) =
(Z.pos (p2 * r2) * (q1 * Z.pos s2)
 ?= Z.pos (p2 * r2) * (s1 * Z.pos q2))
  change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2).p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(Z.pos q2 * Z.pos s2 * (p1 * Z.pos r2)
 ?= Z.pos q2 * Z.pos s2 * (r1 * Z.pos p2)) =
(Z.pos (p2 * r2) * (q1 * Z.pos s2)
 ?= Z.pos (p2 * r2) * (s1 * Z.pos q2))
  change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2).p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(Z.pos q2 * Z.pos s2 * (p1 * Z.pos r2)
 ?= Z.pos q2 * Z.pos s2 * (r1 * Z.pos p2)) =
(Z.pos p2 * Z.pos r2 * (q1 * Z.pos s2)
 ?= Z.pos p2 * Z.pos r2 * (s1 * Z.pos q2))
  replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(p1 * Z.pos q2 * Z.pos r2 * Z.pos s2
 ?= Z.pos q2 * Z.pos s2 * (r1 * Z.pos p2)) =
(Z.pos p2 * Z.pos r2 * (q1 * Z.pos s2)
 ?= Z.pos p2 * Z.pos r2 * (s1 * Z.pos q2))
  rewrite H.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(q1 * Z.pos p2 * Z.pos r2 * Z.pos s2
 ?= Z.pos q2 * Z.pos s2 * (r1 * Z.pos p2)) =
(Z.pos p2 * Z.pos r2 * (q1 * Z.pos s2)
 ?= Z.pos p2 * Z.pos r2 * (s1 * Z.pos q2))
  replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(q1 * Z.pos p2 * Z.pos r2 * Z.pos s2
 ?= r1 * Z.pos s2 * Z.pos q2 * Z.pos p2) =
(Z.pos p2 * Z.pos r2 * (q1 * Z.pos s2)
 ?= Z.pos p2 * Z.pos r2 * (s1 * Z.pos q2))
  rewrite H'.p1:Z
p2:positive
q1:Z
q2:positive
H:p1 * Z.pos q2 = q1 * Z.pos p2
r1:Z
r2:positive
s1:Z
s2:positive
H':r1 * Z.pos s2 = s1 * Z.pos r2
(q1 * Z.pos p2 * Z.pos r2 * Z.pos s2
 ?= s1 * Z.pos r2 * Z.pos q2 * Z.pos p2) =
(Z.pos p2 * Z.pos r2 * (q1 * Z.pos s2)
 ?= Z.pos p2 * Z.pos r2 * (s1 * Z.pos q2))
  f_equal; ring.
  Close Scope Z_scope.
Qed.

Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle.Proper (Qeq ==> Qeq ==> iff) Qle
Proof.Proper (Qeq ==> Qeq ==> iff) Qle
  intros p q H r s H'.p, q:Q
H:p == q
r, s:Q
H':r == s
p <= r <-> q <= s rewrite 2 Qle_alt, H, H'; auto with *.
Qed.

Instance Qlt_compat : Proper (Qeq==>Qeq==>iff) Qlt.Proper (Qeq ==> Qeq ==> iff) Qlt
Proof.Proper (Qeq ==> Qeq ==> iff) Qlt
  intros p q H r s H'.p, q:Q
H:p == q
r, s:Q
H':r == s
p < r <-> q < s rewrite 2 Qlt_alt, H, H'; auto with *.
Qed.

Instance Qeqb_comp : Proper (Qeq==>Qeq==>eq) Qeq_bool.Proper (Qeq ==> Qeq ==> eq) Qeq_bool
Proof.Proper (Qeq ==> Qeq ==> eq) Qeq_bool
 intros p q H r s H'; apply eq_true_iff_eq.p, q:Q
H:p == q
r, s:Q
H':r == s
Qeq_bool p r = true <-> Qeq_bool q s = true
 rewrite 2 Qeq_bool_iff, H, H'; split; auto with qarith.
Qed.

Instance Qleb_comp : Proper (Qeq==>Qeq==>eq) Qle_bool.Proper (Qeq ==> Qeq ==> eq) Qle_bool
Proof.Proper (Qeq ==> Qeq ==> eq) Qle_bool
 intros p q H r s H'; apply eq_true_iff_eq.p, q:Q
H:p == q
r, s:Q
H':r == s
Qle_bool p r = true <-> Qle_bool q s = true
 rewrite 2 Qle_bool_iff, H, H'; split; auto with qarith.
Qed.

0 and 1 are apart

Lemma Q_apart_0_1 : ~ 1 == 0.~ 1 == 0
Proof.~ 1 == 0
  unfold Qeq; auto with qarith.
Qed.

Properties of Qadd

Addition is associative:

Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z.forall x y z : Q, x + (y + z) == x + y + z
Proof.forall x y z : Q, x + (y + z) == x + y + z
  intros (x1, x2) (y1, y2) (z1, z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
(x1 # x2) + ((y1 # y2) + (z1 # z2)) ==
(x1 # x2) + (y1 # y2) + (z1 # z2)
  unfold Qeq, Qplus; simpl; simpl_mult; ring.
Qed.

0 is a neutral element for addition:

Lemma Qplus_0_l : forall x, 0+x == x.forall x : Q, 0 + x == x
Proof.forall x : Q, 0 + x == x
  intros (x1, x2); unfold Qeq, Qplus; simpl; ring.
Qed.

Lemma Qplus_0_r : forall x, x+0 == x.forall x : Q, x + 0 == x
Proof.forall x : Q, x + 0 == x
  intros (x1, x2); unfold Qeq, Qplus; simpl.x1:Z
x2:positive
((x1 * 1 + 0) * Z.pos x2)%Z = (x1 * Z.pos (x2 * 1))%Z
  rewrite Pos.mul_comm; simpl; ring.
Qed.

Commutativity of addition:

Theorem Qplus_comm : forall x y, x+y == y+x.forall x y : Q, x + y == y + x
Proof.forall x y : Q, x + y == y + x
  intros (x1, x2); unfold Qeq, Qplus; simpl.x1:Z
x2:positive
forall y : Q,
((x1 * QDen y + Qnum y * Z.pos x2) *
 Z.pos (Qden y * x2))%Z =
((Qnum y * Z.pos x2 + x1 * QDen y) *
 Z.pos (x2 * Qden y))%Z
  intros; rewrite Pos.mul_comm; ring.
Qed.

Properties of Qopp

Lemma Qopp_involutive : forall q, - -q == q.forall q : Q, - - q == q
Proof.forall q : Q, - - q == q
  red; simpl; intros; ring.
Qed.

Theorem Qplus_opp_r : forall q, q+(-q) == 0.forall q : Q, q + - q == 0
Proof.forall q : Q, q + - q == 0
  red; simpl; intro; ring.
Qed.

Injectivity of addition (uses theory about Qopp above):

Lemma Qplus_inj_r (x y z: Q):
  x + z == y + z <-> x == y.x, y, z:Q
x + z == y + z <-> x == y
Proof.x, y, z:Q
x + z == y + z <-> x == y
 split; intro E.x, y, z:Q
E:x + z == y + z
x == y
x, y, z:Q
E:x == y
x + z == y + z
  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y).x, y, z:Q
E:x + z == y + z
x + 0 == y + 0
x, y, z:Q
E:x == y
x + z == y + z
  rewrite <- (Qplus_opp_r z); auto.x, y, z:Q
E:x + z == y + z
x + (z + - z) == y + (z + - z)
x, y, z:Q
E:x == y
x + z == y + z
  do 2 rewrite Qplus_assoc.x, y, z:Q
E:x + z == y + z
x + z + - z == y + z + - z
x, y, z:Q
E:x == y
x + z == y + z
  rewrite E.x, y, z:Q
E:x + z == y + z
y + z + - z == y + z + - z
x, y, z:Q
E:x == y
x + z == y + z reflexivity.x, y, z:Q
E:x == y
x + z == y + z
 rewrite E.x, y, z:Q
E:x == y
y + z == y + z reflexivity.
Qed.

Lemma Qplus_inj_l (x y z: Q):
  z + x == z + y <-> x == y.x, y, z:Q
z + x == z + y <-> x == y
Proof.x, y, z:Q
z + x == z + y <-> x == y
 rewrite (Qplus_comm z x), (Qplus_comm z y).x, y, z:Q
x + z == y + z <-> x == y
 apply Qplus_inj_r.
Qed.

Properties of Qmult

Multiplication is associative:

Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p.forall n m p : Q, n * (m * p) == n * m * p
Proof.forall n m p : Q, n * (m * p) == n * m * p
  intros; red; simpl; rewrite Pos.mul_assoc; ring.
Qed.

multiplication and zero

Lemma Qmult_0_l : forall x , 0*x == 0.forall x : Q, 0 * x == 0
Proof.forall x : Q, 0 * x == 0
  intros; compute; reflexivity.
Qed.

Lemma Qmult_0_r : forall x , x*0 == 0.forall x : Q, x * 0 == 0
Proof.forall x : Q, x * 0 == 0
  intros; red; simpl; ring.
Qed.

1 is a neutral element for multiplication:

Lemma Qmult_1_l : forall n, 1*n == n.forall n : Q, 1 * n == n
Proof.forall n : Q, 1 * n == n
  intro; red; simpl; destruct (Qnum n); auto.
Qed.

Theorem Qmult_1_r : forall n, n*1==n.forall n : Q, n * 1 == n
Proof.forall n : Q, n * 1 == n
  intro; red; simpl.n:Q
(Qnum n * 1 * QDen n)%Z =
(Qnum n * Z.pos (Qden n * 1))%Z
  rewrite Z.mul_1_r with (n := Qnum n).n:Q
(Qnum n * QDen n)%Z = (Qnum n * Z.pos (Qden n * 1))%Z
  rewrite Pos.mul_comm; simpl; trivial.
Qed.

Commutativity of multiplication

Theorem Qmult_comm : forall x y, x*y==y*x.forall x y : Q, x * y == y * x
Proof.forall x y : Q, x * y == y * x
  intros; red; simpl; rewrite Pos.mul_comm; ring.
Qed.

Distributivity over Qadd

Theorem Qmult_plus_distr_r : forall x y z, x*(y+z)==(x*y)+(x*z).forall x y z : Q, x * (y + z) == x * y + x * z
Proof.forall x y z : Q, x * (y + z) == x * y + x * z
  intros (x1, x2) (y1, y2) (z1, z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
(x1 # x2) * ((y1 # y2) + (z1 # z2)) ==
(x1 # x2) * (y1 # y2) + (x1 # x2) * (z1 # z2)
  unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring.
Qed.

Theorem Qmult_plus_distr_l : forall x y z, (x+y)*z==(x*z)+(y*z).forall x y z : Q, (x + y) * z == x * z + y * z
Proof.forall x y z : Q, (x + y) * z == x * z + y * z
  intros (x1, x2) (y1, y2) (z1, z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
((x1 # x2) + (y1 # y2)) * (z1 # z2) ==
(x1 # x2) * (z1 # z2) + (y1 # y2) * (z1 # z2)
  unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring.
Qed.

Integrality

Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0.forall x y : Q, x * y == 0 -> x == 0 \/ y == 0
Proof.forall x y : Q, x * y == 0 -> x == 0 \/ y == 0
  intros (x1,x2) (y1,y2).x1:Z
x2:positive
y1:Z
y2:positive
(x1 # x2) * (y1 # y2) == 0 ->
x1 # x2 == 0 \/ y1 # y2 == 0
  unfold Qeq, Qmult; simpl.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * y1 * 1)%Z = 0%Z ->
(x1 * 1)%Z = 0%Z \/ (y1 * 1)%Z = 0%Z
  now rewrite <- Z.mul_eq_0, !Z.mul_1_r.
Qed.

Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.forall x y : Q, ~ x == 0 -> x * y == 0 -> y == 0
Proof.forall x y : Q, ~ x == 0 -> x * y == 0 -> y == 0
  intros (x1, x2) (y1, y2).x1:Z
x2:positive
y1:Z
y2:positive
~ x1 # x2 == 0 ->
(x1 # x2) * (y1 # y2) == 0 -> y1 # y2 == 0
  unfold Qeq, Qmult; simpl.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * 1)%Z <> 0%Z ->
(x1 * y1 * 1)%Z = 0%Z -> (y1 * 1)%Z = 0%Z
  rewrite !Z.mul_1_r, Z.mul_eq_0.x1:Z
x2:positive
y1:Z
y2:positive
x1 <> 0%Z -> x1 = 0%Z \/ y1 = 0%Z -> y1 = 0%Z intuition.
Qed.

inject_Z is a ring homomorphism:

Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y.x, y:Z
inject_Z (x + y) = inject_Z x + inject_Z y
Proof.x, y:Z
inject_Z (x + y) = inject_Z x + inject_Z y
 unfold Qplus, inject_Z.x, y:Z
x + y # 1 =
Qnum (x # 1) * QDen (y # 1) +
Qnum (y # 1) * QDen (x # 1)
# Qden (x # 1) * Qden (y # 1) simpl.x, y:Z
x + y # 1 = x * 1 + y * 1 # 1 f_equal.x, y:Z
(x + y)%Z = (x * 1 + y * 1)%Z ring.
Qed.

Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y.x, y:Z
inject_Z (x * y) = inject_Z x * inject_Z y
Proof.x, y:Z
inject_Z (x * y) = inject_Z x * inject_Z y reflexivity. Qed.

Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x.x:Z
inject_Z (- x) = - inject_Z x
Proof.x:Z
inject_Z (- x) = - inject_Z x reflexivity. Qed.

Inverse and division.

Lemma Qinv_involutive : forall q, (/ / q) == q.forall q : Q, / / q == q
Proof.forall q : Q, / / q == q
intros [[|n|n] d]; red; simpl; reflexivity.
Qed.

Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.forall x : Q, ~ x == 0 -> x * / x == 1
Proof.forall x : Q, ~ x == 0 -> x * / x == 1
  intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl;
    intros; simpl_mult; try ring.x1:Z
x2:positive
H:0%Z <> 0%Z
0%Z = (Z.pos x2 * 1)%Z
  elim H; auto.
Qed.

Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.forall p q : Q, / (p * q) == / p * / q
Proof.forall p q : Q, / (p * q) == / p * / q
  intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl.x1:Z
x2:positive
y1:Z
y2:positive
(Qnum
   match x1 * y1 with
   | 0%Z => 0
   | Z.pos p => Z.pos (x2 * y2) # p
   | Z.neg p => Z.neg (x2 * y2) # p
   end *
 Z.pos
   (Qden
      match x1 with
      | 0%Z => 0
      | Z.pos p => Z.pos x2 # p
      | Z.neg p => Z.neg x2 # p
      end *
    Qden
      match y1 with
      | 0%Z => 0
      | Z.pos p => Z.pos y2 # p
      | Z.neg p => Z.neg y2 # p
      end))%Z =
(Qnum
   match x1 with
   | 0%Z => 0
   | Z.pos p => Z.pos x2 # p
   | Z.neg p => Z.neg x2 # p
   end *
 Qnum
   match y1 with
   | 0%Z => 0
   | Z.pos p => Z.pos y2 # p
   | Z.neg p => Z.neg y2 # p
   end *
 QDen
   match x1 * y1 with
   | 0%Z => 0
   | Z.pos p => Z.pos (x2 * y2) # p
   | Z.neg p => Z.neg (x2 * y2) # p
   end)%Z
  destruct x1; simpl; auto;
    destruct y1; simpl; auto.
Qed.

Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.forall x y : Q, ~ y == 0 -> x * y / y == x
Proof.forall x y : Q, ~ y == 0 -> x * y / y == x
  intros; unfold Qdiv.x, y:Q
H:~ y == 0
x * y * / y == x
  rewrite <- (Qmult_assoc x y (Qinv y)).x, y:Q
H:~ y == 0
x * (y * / y) == x
  rewrite (Qmult_inv_r y H).x, y:Q
H:~ y == 0
x * 1 == x
  apply Qmult_1_r.
Qed.

Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.forall x y : Q, ~ y == 0 -> y * (x / y) == x
Proof.forall x y : Q, ~ y == 0 -> y * (x / y) == x
  intros; unfold Qdiv.x, y:Q
H:~ y == 0
y * (x * / y) == x
  rewrite (Qmult_assoc y x (Qinv y)).x, y:Q
H:~ y == 0
y * x * / y == x
  rewrite (Qmult_comm y x).x, y:Q
H:~ y == 0
x * y * / y == x
  fold (Qdiv (Qmult x y) y).x, y:Q
H:~ y == 0
x * y / y == x
  apply Qdiv_mult_l; auto.
Qed.

Injectivity of Qmult (requires theory about Qinv above):

Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y).x, y, z:Q
~ z == 0 -> x * z == y * z <-> x == y
Proof.x, y, z:Q
~ z == 0 -> x * z == y * z <-> x == y
 intro z_ne_0.x, y, z:Q
z_ne_0:~ z == 0
x * z == y * z <-> x == y
 split; intro E.x, y, z:Q
z_ne_0:~ z == 0
E:x * z == y * z
x == y
x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z
  rewrite <- (Qmult_1_r x), <- (Qmult_1_r y).x, y, z:Q
z_ne_0:~ z == 0
E:x * z == y * z
x * 1 == y * 1
x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z
  rewrite <- (Qmult_inv_r z); auto.x, y, z:Q
z_ne_0:~ z == 0
E:x * z == y * z
x * (z * / z) == y * (z * / z)
x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z
  do 2 rewrite Qmult_assoc.x, y, z:Q
z_ne_0:~ z == 0
E:x * z == y * z
x * z * / z == y * z * / z
x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z
  rewrite E.x, y, z:Q
z_ne_0:~ z == 0
E:x * z == y * z
y * z * / z == y * z * / z
x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z reflexivity.x, y, z:Q
z_ne_0:~ z == 0
E:x == y
x * z == y * z
 rewrite E.x, y, z:Q
z_ne_0:~ z == 0
E:x == y
y * z == y * z reflexivity.
Qed.

Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y).x, y, z:Q
~ z == 0 -> z * x == z * y <-> x == y
Proof.x, y, z:Q
~ z == 0 -> z * x == z * y <-> x == y
 rewrite (Qmult_comm z x), (Qmult_comm z y).x, y, z:Q
~ z == 0 -> x * z == y * z <-> x == y
 apply Qmult_inj_r.
Qed.

Properties of order upon Q.

Lemma Qle_refl x : x<=x.x:Q
x <= x
Proof.x:Q
x <= x
  unfold Qle; auto with zarith.
Qed.

Lemma Qle_antisym x y : x<=y -> y<=x -> x==y.x, y:Q
x <= y -> y <= x -> x == y
Proof.x, y:Q
x <= y -> y <= x -> x == y
  unfold Qle, Qeq; auto with zarith.
Qed.

Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.forall x y z : Q, x <= y -> y <= z -> x <= z
Proof.forall x y z : Q, x <= y -> y <= z -> x <= z
  unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
H0:(y1 * Z.pos z2 <= z1 * Z.pos y2)%Z
(x1 * Z.pos z2 <= z1 * Z.pos x2)%Z
  Open Scope Z_scope.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 <= z1 * Z.pos x2
  apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|].x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 <= z1 * Z.pos x2 * Z.pos y2
  apply Z.le_trans with (y1 * Zpos x2 * Zpos z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 <= y1 * Z.pos x2 * Z.pos z2
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 <= z1 * Z.pos x2 * Z.pos y2
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 <= y1 * Z.pos x2 * Z.pos z2 rewrite Z.mul_shuffle0.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos y2 * Z.pos z2 <= y1 * Z.pos x2 * Z.pos z2 now apply Z.mul_le_mono_pos_r.
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 <= z1 * Z.pos x2 * Z.pos y2 rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos z2 * Z.pos x2 <= z1 * Z.pos y2 * Z.pos x2
    now apply Z.mul_le_mono_pos_r.
  Close Scope Z_scope.
Qed.

Hint Resolve Qle_trans : qarith.

Lemma Qlt_irrefl x : ~x<x.x:Q
~ x < x
Proof.x:Q
~ x < x
 unfold Qlt.x:Q
~ (Qnum x * QDen x < Qnum x * QDen x)%Z auto with zarith.
Qed.

Lemma Qlt_not_eq x y : x<y -> ~ x==y.x, y:Q
x < y -> ~ x == y
Proof.x, y:Q
x < y -> ~ x == y
  unfold Qlt, Qeq; auto with zarith.
Qed.

Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y).x, y:Z
(x <= y)%Z = (inject_Z x <= inject_Z y)
Proof.x, y:Z
(x <= y)%Z = (inject_Z x <= inject_Z y)
 unfold Qle.x, y:Z
(x <= y)%Z =
(Qnum (inject_Z x) * QDen (inject_Z y) <=
 Qnum (inject_Z y) * QDen (inject_Z x))%Z simpl.x, y:Z
(x <= y)%Z = (x * 1 <= y * 1)%Z now rewrite !Z.mul_1_r.
Qed.

Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y).x, y:Z
(x < y)%Z = (inject_Z x < inject_Z y)
Proof.x, y:Z
(x < y)%Z = (inject_Z x < inject_Z y)
 unfold Qlt.x, y:Z
(x < y)%Z =
(Qnum (inject_Z x) * QDen (inject_Z y) <
 Qnum (inject_Z y) * QDen (inject_Z x))%Z simpl.x, y:Z
(x < y)%Z = (x * 1 < y * 1)%Z now rewrite !Z.mul_1_r.
Qed.

Large = strict or equal

Lemma Qle_lteq x y : x<=y <-> x<y \/ x==y.x, y:Q
x <= y <-> x < y \/ x == y
Proof.x, y:Q
x <= y <-> x < y \/ x == y
 rewrite Qeq_alt, Qle_alt, Qlt_alt.x, y:Q
(x ?= y) <> Gt <-> (x ?= y) = Lt \/ (x ?= y) = Eq
 destruct (x ?= y); intuition; discriminate.
Qed.

Lemma Qlt_le_weak x y : x<y -> x<=y.x, y:Q
x < y -> x <= y
Proof.x, y:Q
x < y -> x <= y
  unfold Qle, Qlt; auto with zarith.
Qed.

Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.forall x y z : Q, x <= y -> y < z -> x < z
Proof.forall x y z : Q, x <= y -> y < z -> x < z
  unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
H0:(y1 * Z.pos z2 < z1 * Z.pos y2)%Z
(x1 * Z.pos z2 < z1 * Z.pos x2)%Z
  Open Scope Z_scope.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
x1 * Z.pos z2 < z1 * Z.pos x2
  apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 < z1 * Z.pos x2 * Z.pos y2
  apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 <= y1 * Z.pos x2 * Z.pos z2
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 < z1 * Z.pos x2 * Z.pos y2
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 <= y1 * Z.pos x2 * Z.pos z2 rewrite Z.mul_shuffle0.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
x1 * Z.pos y2 * Z.pos z2 <= y1 * Z.pos x2 * Z.pos z2 now apply Z.mul_le_mono_pos_r.
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 < z1 * Z.pos x2 * Z.pos y2 rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:y1 * Z.pos z2 < z1 * Z.pos y2
y1 * Z.pos z2 * Z.pos x2 < z1 * Z.pos y2 * Z.pos x2
    now apply Z.mul_lt_mono_pos_r.
  Close Scope Z_scope.
Qed.

Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.forall x y z : Q, x < y -> y <= z -> x < z
Proof.forall x y z : Q, x < y -> y <= z -> x < z
  unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
H0:(y1 * Z.pos z2 <= z1 * Z.pos y2)%Z
(x1 * Z.pos z2 < z1 * Z.pos x2)%Z
  Open Scope Z_scope.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 < z1 * Z.pos x2
  apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 < z1 * Z.pos x2 * Z.pos y2
  apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 < y1 * Z.pos x2 * Z.pos z2
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 <= z1 * Z.pos x2 * Z.pos y2
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos z2 * Z.pos y2 < y1 * Z.pos x2 * Z.pos z2 rewrite Z.mul_shuffle0.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
x1 * Z.pos y2 * Z.pos z2 < y1 * Z.pos x2 * Z.pos z2 now apply Z.mul_lt_mono_pos_r.
  -x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos x2 * Z.pos z2 <= z1 * Z.pos x2 * Z.pos y2 rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:y1 * Z.pos z2 <= z1 * Z.pos y2
y1 * Z.pos z2 * Z.pos x2 <= z1 * Z.pos y2 * Z.pos x2
    now apply Z.mul_le_mono_pos_r.
  Close Scope Z_scope.
Qed.

Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.forall x y z : Q, x < y -> y < z -> x < z
Proof.forall x y z : Q, x < y -> y < z -> x < z
  intros.x, y, z:Q
H:x < y
H0:y < z
x < z
  apply Qle_lt_trans with y; auto.x, y, z:Q
H:x < y
H0:y < z
x <= y
  apply Qlt_le_weak; auto.
Qed.

x<y iff ~(y≤x)

Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x.forall x y : Q, ~ x < y -> y <= x
Proof.forall x y : Q, ~ x < y -> y <= x
  unfold Qle, Qlt; auto with zarith.
Qed.

Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x.forall x y : Q, ~ x <= y -> y < x
Proof.forall x y : Q, ~ x <= y -> y < x
  unfold Qle, Qlt; auto with zarith.
Qed.

Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x.forall x y : Q, x < y -> ~ y <= x
Proof.forall x y : Q, x < y -> ~ y <= x
  unfold Qle, Qlt; auto with zarith.
Qed.

Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x.forall x y : Q, x <= y -> ~ y < x
Proof.forall x y : Q, x <= y -> ~ y < x
  unfold Qle, Qlt; auto with zarith.
Qed.

Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.forall x y : Q, x <= y -> x < y \/ x == y
Proof.forall x y : Q, x <= y -> x < y \/ x == y
  unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases.
Qed.

Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
 Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith.

Some decidability results about orders.

Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}.forall x y : Q, {x < y} + {y < x} + {x == y}
Proof.forall x y : Q, {x < y} + {y < x} + {x == y}
  unfold Qlt, Qle, Qeq; intros.x, y:Q
{(Qnum x * QDen y < Qnum y * QDen x)%Z} +
{(Qnum y * QDen x < Qnum x * QDen y)%Z} +
{(Qnum x * QDen y)%Z = (Qnum y * QDen x)%Z}
  exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)).
Defined.

Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}.forall x y : Q, {x < y} + {y <= x}
Proof.forall x y : Q, {x < y} + {y <= x}
  unfold Qlt, Qle; intros.x, y:Q
{(Qnum x * QDen y < Qnum y * QDen x)%Z} +
{(Qnum y * QDen x <= Qnum x * QDen y)%Z}
  exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)).
Defined.

Compatibility of operations with respect to order.

Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.forall p q : Q, p <= q -> - q <= - p
Proof.forall p q : Q, p <= q -> - q <= - p
  intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
(a1 * Z.pos b2 <= b1 * Z.pos a2)%Z ->
(- b1 * Z.pos a2 <= - a1 * Z.pos b2)%Z
  rewrite !Z.mul_opp_l.a1:Z
a2:positive
b1:Z
b2:positive
(a1 * Z.pos b2 <= b1 * Z.pos a2)%Z ->
(- (b1 * Z.pos a2) <= - (a1 * Z.pos b2))%Z omega.
Qed.

Hint Resolve Qopp_le_compat : qarith.

Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.forall p q : Q, p <= q <-> 0 <= q + - p
Proof.forall p q : Q, p <= q <-> 0 <= q + - p
  intros (x1,x2) (y1,y2); unfold Qle; simpl.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z <->
(0 <= (y1 * Z.pos x2 + - x1 * Z.pos y2) * 1)%Z
  rewrite Z.mul_opp_l.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z <->
(0 <= (y1 * Z.pos x2 + - (x1 * Z.pos y2)) * 1)%Z omega.
Qed.

Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.forall p q : Q, p < q <-> 0 < q + - p
Proof.forall p q : Q, p < q <-> 0 < q + - p
  intros (x1,x2) (y1,y2); unfold Qlt; simpl.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * Z.pos y2 < y1 * Z.pos x2)%Z <->
(0 < (y1 * Z.pos x2 + - x1 * Z.pos y2) * 1)%Z
  rewrite Z.mul_opp_l.x1:Z
x2:positive
y1:Z
y2:positive
(x1 * Z.pos y2 < y1 * Z.pos x2)%Z <->
(0 < (y1 * Z.pos x2 + - (x1 * Z.pos y2)) * 1)%Z omega.
Qed.

Lemma Qplus_le_compat :
  forall x y z t, x<=y -> z<=t -> x+z <= y+t.forall x y z t : Q, x <= y -> z <= t -> x + z <= y + t
Proof.forall x y z t : Q, x <= y -> z <= t -> x + z <= y + t
  unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
    simpl; simpl_mult.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z ->
(z1 * Z.pos t2 <= t1 * Z.pos z2)%Z ->
((x1 * Z.pos z2 + z1 * Z.pos x2) *
 (Z.pos y2 * Z.pos t2) <=
 (y1 * Z.pos t2 + t1 * Z.pos y2) *
 (Z.pos x2 * Z.pos z2))%Z
  Open Scope Z_scope.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
x1 * Z.pos y2 <= y1 * Z.pos x2 ->
z1 * Z.pos t2 <= t1 * Z.pos z2 ->
(x1 * Z.pos z2 + z1 * Z.pos x2) *
(Z.pos y2 * Z.pos t2) <=
(y1 * Z.pos t2 + t1 * Z.pos y2) *
(Z.pos x2 * Z.pos z2)
  intros.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
(x1 * Z.pos z2 + z1 * Z.pos x2) *
(Z.pos y2 * Z.pos t2) <=
(y1 * Z.pos t2 + t1 * Z.pos y2) *
(Z.pos x2 * Z.pos z2)
  match goal with |- ?a <= ?b => ring_simplify a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 +
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1 +
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  rewrite Z.add_comm.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 +
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1 +
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  apply Z.add_le_mono.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos t2 * Z.pos x2 * Z.pos y2 <=
t1 * Z.pos z2 * Z.pos x2 * Z.pos y2
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  auto with zarith.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 <= y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos y2 * Z.pos z2 * Z.pos t2 <=
y1 * Z.pos x2 * Z.pos z2 * Z.pos t2
  auto with zarith.
  Close Scope Z_scope.
Qed.

Lemma Qplus_lt_le_compat :
  forall x y z t, x<y -> z<=t -> x+z < y+t.forall x y z t : Q, x < y -> z <= t -> x + z < y + t
Proof.forall x y z t : Q, x < y -> z <= t -> x + z < y + t
  unfold Qplus, Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
    simpl; simpl_mult.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
(x1 * Z.pos y2 < y1 * Z.pos x2)%Z ->
(z1 * Z.pos t2 <= t1 * Z.pos z2)%Z ->
((x1 * Z.pos z2 + z1 * Z.pos x2) *
 (Z.pos y2 * Z.pos t2) <
 (y1 * Z.pos t2 + t1 * Z.pos y2) *
 (Z.pos x2 * Z.pos z2))%Z
  Open Scope Z_scope.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
x1 * Z.pos y2 < y1 * Z.pos x2 ->
z1 * Z.pos t2 <= t1 * Z.pos z2 ->
(x1 * Z.pos z2 + z1 * Z.pos x2) *
(Z.pos y2 * Z.pos t2) <
(y1 * Z.pos t2 + t1 * Z.pos y2) *
(Z.pos x2 * Z.pos z2)
  intros.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
(x1 * Z.pos z2 + z1 * Z.pos x2) *
(Z.pos y2 * Z.pos t2) <
(y1 * Z.pos t2 + t1 * Z.pos y2) *
(Z.pos x2 * Z.pos z2)
  match goal with |- ?a < ?b => ring_simplify a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 +
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 <
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1 +
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  rewrite Z.add_comm.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 +
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1 +
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  apply Z.add_le_lt_mono.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos x2 * Z.pos y2 * Z.pos t2 <=
Z.pos z2 * Z.pos x2 * Z.pos y2 * t1
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
z1 * Z.pos t2 * Z.pos x2 * Z.pos y2 <=
t1 * Z.pos z2 * Z.pos x2 * Z.pos y2
x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  auto with zarith.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos z2 * Z.pos y2 * Z.pos t2 <
Z.pos z2 * Z.pos x2 * Z.pos t2 * y1
  match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.x1:Z
x2:positive
y1:Z
y2:positive
z1:Z
z2:positive
t1:Z
t2:positive
H:x1 * Z.pos y2 < y1 * Z.pos x2
H0:z1 * Z.pos t2 <= t1 * Z.pos z2
x1 * Z.pos y2 * Z.pos z2 * Z.pos t2 <
y1 * Z.pos x2 * Z.pos z2 * Z.pos t2
  do 2 (apply Z.mul_lt_mono_pos_r;try easy).
  Close Scope Z_scope.
Qed.

Lemma Qplus_le_l (x y z: Q): x + z <= y + z <-> x <= y.x, y, z:Q
x + z <= y + z <-> x <= y
Proof.x, y, z:Q
x + z <= y + z <-> x <= y
 split; intros.x, y, z:Q
H:x + z <= y + z
x <= y
x, y, z:Q
H:x <= y
x + z <= y + z
  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z).x, y, z:Q
H:x + z <= y + z
x + (z + - z) <= y + (z + - z)
x, y, z:Q
H:x <= y
x + z <= y + z
  do 2 rewrite Qplus_assoc.x, y, z:Q
H:x + z <= y + z
x + z + - z <= y + z + - z
x, y, z:Q
H:x <= y
x + z <= y + z
  apply Qplus_le_compat; auto with *.x, y, z:Q
H:x <= y
x + z <= y + z
 apply Qplus_le_compat; auto with *.
Qed.

Lemma Qplus_le_r (x y z: Q): z + x <= z + y <-> x <= y.x, y, z:Q
z + x <= z + y <-> x <= y
Proof.x, y, z:Q
z + x <= z + y <-> x <= y
 rewrite (Qplus_comm z x), (Qplus_comm z y).x, y, z:Q
x + z <= y + z <-> x <= y
 apply Qplus_le_l.
Qed.

Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y.x, y, z:Q
x + z < y + z <-> x < y
Proof.x, y, z:Q
x + z < y + z <-> x < y
 split; intros.x, y, z:Q
H:x + z < y + z
x < y
x, y, z:Q
H:x < y
x + z < y + z
  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z).x, y, z:Q
H:x + z < y + z
x + (z + - z) < y + (z + - z)
x, y, z:Q
H:x < y
x + z < y + z
  do 2 rewrite Qplus_assoc.x, y, z:Q
H:x + z < y + z
x + z + - z < y + z + - z
x, y, z:Q
H:x < y
x + z < y + z
  apply Qplus_lt_le_compat; auto with *.x, y, z:Q
H:x < y
x + z < y + z
 apply Qplus_lt_le_compat; auto with *.
Qed.

Lemma Qplus_lt_r (x y z: Q): z + x < z + y <-> x < y.x, y, z:Q
z + x < z + y <-> x < y
Proof.x, y, z:Q
z + x < z + y <-> x < y
 rewrite (Qplus_comm z x), (Qplus_comm z y).x, y, z:Q
x + z < y + z <-> x < y
 apply Qplus_lt_l.
Qed.

Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.forall x y z : Q, x <= y -> 0 <= z -> x * z <= y * z
Proof.forall x y z : Q, x <= y -> 0 <= z -> x * z <= y * z
  intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
(a1 * Z.pos b2 <= b1 * Z.pos a2)%Z ->
(0 <= c1 * 1)%Z ->
(a1 * c1 * Z.pos (b2 * c2) <=
 b1 * c1 * Z.pos (a2 * c2))%Z
  Open Scope Z_scope.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
a1 * Z.pos b2 <= b1 * Z.pos a2 ->
0 <= c1 * 1 ->
a1 * c1 * Z.pos (b2 * c2) <= b1 * c1 * Z.pos (a2 * c2)
  intros; simpl_mult.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
H:a1 * Z.pos b2 <= b1 * Z.pos a2
H0:0 <= c1 * 1
a1 * c1 * (Z.pos b2 * Z.pos c2) <=
b1 * c1 * (Z.pos a2 * Z.pos c2)
  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
H:a1 * Z.pos b2 <= b1 * Z.pos a2
H0:0 <= c1 * 1
a1 * Z.pos b2 * (c1 * Z.pos c2) <=
b1 * Z.pos a2 * (c1 * Z.pos c2)
  apply Z.mul_le_mono_nonneg_r; auto with zarith.
  Close Scope Z_scope.
Qed.

Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z  -> x*z <= y*z -> x <= y.forall x y z : Q, 0 < z -> x * z <= y * z -> x <= y
Proof.forall x y z : Q, 0 < z -> x * z <= y * z -> x <= y
  intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
(0 < c1 * 1)%Z ->
(a1 * c1 * Z.pos (b2 * c2) <=
 b1 * c1 * Z.pos (a2 * c2))%Z ->
(a1 * Z.pos b2 <= b1 * Z.pos a2)%Z
  Open Scope Z_scope.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * c1 * Z.pos (b2 * c2) <= b1 * c1 * Z.pos (a2 * c2) ->
a1 * Z.pos b2 <= b1 * Z.pos a2
  simpl_mult.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * c1 * (Z.pos b2 * Z.pos c2) <=
b1 * c1 * (Z.pos a2 * Z.pos c2) ->
a1 * Z.pos b2 <= b1 * Z.pos a2
  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * Z.pos b2 * (c1 * Z.pos c2) <=
b1 * Z.pos a2 * (c1 * Z.pos c2) ->
a1 * Z.pos b2 <= b1 * Z.pos a2
  intros LT LE.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
LE:a1 * Z.pos b2 * (c1 * Z.pos c2) <=
b1 * Z.pos a2 * (c1 * Z.pos c2)
a1 * Z.pos b2 <= b1 * Z.pos a2
  apply Z.mul_le_mono_pos_r in LE; trivial.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
LE:a1 * Z.pos b2 * (c1 * Z.pos c2) <=
b1 * Z.pos a2 * (c1 * Z.pos c2)
H:forall n m p : Z,
0 < p -> n * p <= m * p -> n <= m
0 < c1 * Z.pos c2
  apply Z.mul_pos_pos; [omega|easy].
  Close Scope Z_scope.
Qed.

Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y).x, y, z:Q
0 < z -> x * z <= y * z <-> x <= y
Proof.x, y, z:Q
0 < z -> x * z <= y * z <-> x <= y
 split; intro.x, y, z:Q
H:0 < z
H0:x * z <= y * z
x <= y
x, y, z:Q
H:0 < z
H0:x <= y
x * z <= y * z
  now apply Qmult_lt_0_le_reg_r with z.x, y, z:Q
H:0 < z
H0:x <= y
x * z <= y * z
 apply Qmult_le_compat_r; auto with qarith.
Qed.

Lemma Qmult_le_l (x y z: Q): 0 < z -> (z*x <= z*y <-> x <= y).x, y, z:Q
0 < z -> z * x <= z * y <-> x <= y
Proof.x, y, z:Q
0 < z -> z * x <= z * y <-> x <= y
 rewrite (Qmult_comm z x), (Qmult_comm z y).x, y, z:Q
0 < z -> x * z <= y * z <-> x <= y
 apply Qmult_le_r.
Qed.

Lemma Qmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.forall x y z : Q, 0 < z -> x < y -> x * z < y * z
Proof.forall x y z : Q, 0 < z -> x < y -> x * z < y * z
  intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
(0 < c1 * 1)%Z ->
(a1 * Z.pos b2 < b1 * Z.pos a2)%Z ->
(a1 * c1 * Z.pos (b2 * c2) < b1 * c1 * Z.pos (a2 * c2))%Z
  Open Scope Z_scope.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * Z.pos b2 < b1 * Z.pos a2 ->
a1 * c1 * Z.pos (b2 * c2) < b1 * c1 * Z.pos (a2 * c2)
  intros; simpl_mult.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
H:0 < c1 * 1
H0:a1 * Z.pos b2 < b1 * Z.pos a2
a1 * c1 * (Z.pos b2 * Z.pos c2) <
b1 * c1 * (Z.pos a2 * Z.pos c2)
  rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
H:0 < c1 * 1
H0:a1 * Z.pos b2 < b1 * Z.pos a2
a1 * Z.pos b2 * (c1 * Z.pos c2) <
b1 * Z.pos a2 * (c1 * Z.pos c2)
  apply Z.mul_lt_mono_pos_r; auto with zarith.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
H:0 < c1 * 1
H0:a1 * Z.pos b2 < b1 * Z.pos a2
0 < c1 * Z.pos c2
  apply Z.mul_pos_pos; [omega|reflexivity].
  Close Scope Z_scope.
Qed.

Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y).forall x y z : Q, 0 < z -> x * z < y * z <-> x < y
Proof.forall x y z : Q, 0 < z -> x * z < y * z <-> x < y
 Open Scope Z_scope.forall x y z : Q,
(0 < z)%Q -> (x * z < y * z)%Q <-> (x < y)%Q
 intros (a1,a2) (b1,b2) (c1,c2).a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
(0 < c1 # c2)%Q ->
((a1 # a2) * (c1 # c2) < (b1 # b2) * (c1 # c2))%Q <->
(a1 # a2 < b1 # b2)%Q
 unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * c1 * Z.pos (b2 * c2) < b1 * c1 * Z.pos (a2 * c2) <->
a1 * Z.pos b2 < b1 * Z.pos a2
 simpl_mult.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * c1 * (Z.pos b2 * Z.pos c2) <
b1 * c1 * (Z.pos a2 * Z.pos c2) <->
a1 * Z.pos b2 < b1 * Z.pos a2
 rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1).a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
0 < c1 * 1 ->
a1 * Z.pos b2 * (c1 * Z.pos c2) <
b1 * Z.pos a2 * (c1 * Z.pos c2) <->
a1 * Z.pos b2 < b1 * Z.pos a2
 intro LT.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
a1 * Z.pos b2 * (c1 * Z.pos c2) <
b1 * Z.pos a2 * (c1 * Z.pos c2) <->
a1 * Z.pos b2 < b1 * Z.pos a2 rewrite <- Z.mul_lt_mono_pos_r.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
a1 * Z.pos b2 < b1 * Z.pos a2 <->
a1 * Z.pos b2 < b1 * Z.pos a2
a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
0 < c1 * Z.pos c2 reflexivity.a1:Z
a2:positive
b1:Z
b2:positive
c1:Z
c2:positive
LT:0 < c1 * 1
0 < c1 * Z.pos c2
 apply Z.mul_pos_pos; [omega|reflexivity].
 Close Scope Z_scope.
Qed.

Lemma Qmult_lt_l (x y z: Q): 0 < z -> (z*x < z*y <-> x < y).x, y, z:Q
0 < z -> z * x < z * y <-> x < y
Proof.x, y, z:Q
0 < z -> z * x < z * y <-> x < y
 rewrite (Qmult_comm z x), (Qmult_comm z y).x, y, z:Q
0 < z -> x * z < y * z <-> x < y
 apply Qmult_lt_r.
Qed.

Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.forall a b : Q, 0 <= a -> 0 <= b -> 0 <= a * b
Proof.forall a b : Q, 0 <= a -> 0 <= b -> 0 <= a * b
intros a b Ha Hb.a, b:Q
Ha:0 <= a
Hb:0 <= b
0 <= a * b
unfold Qle in *.a, b:Q
Ha:(Qnum 0 * QDen a <= Qnum a * QDen 0)%Z
Hb:(Qnum 0 * QDen b <= Qnum b * QDen 0)%Z
(Qnum 0 * QDen (a * b) <= Qnum (a * b) * QDen 0)%Z
simpl in *.a, b:Q
Ha:(0 <= Qnum a * 1)%Z
Hb:(0 <= Qnum b * 1)%Z
(0 <= Qnum a * Qnum b * 1)%Z
auto with *.
Qed.

Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a.forall a : Q, 0 <= a -> 0 <= / a
Proof.forall a : Q, 0 <= a -> 0 <= / a
intros [[|n|n] d] Ha; assumption.
Qed.

Lemma Qle_shift_div_l : forall a b c,
 0 < c -> a*c <= b -> a <= b/c.forall a b c : Q, 0 < c -> a * c <= b -> a <= b / c
Proof.forall a b c : Q, 0 < c -> a * c <= b -> a <= b / c
intros a b c Hc H.a, b, c:Q
Hc:0 < c
H:a * c <= b
a <= b / c
apply Qmult_lt_0_le_reg_r with (c).a, b, c:Q
Hc:0 < c
H:a * c <= b
0 < c
a, b, c:Q
Hc:0 < c
H:a * c <= b
a * c <= b / c * c
 assumption.a, b, c:Q
Hc:0 < c
H:a * c <= b
a * c <= b / c * c
setoid_replace (b/c*c) with (c*(b/c)) by apply Qmult_comm.a, b, c:Q
Hc:0 < c
H:a * c <= b
a * c <= c * (b / c)
rewrite Qmult_div_r; try assumption.a, b, c:Q
Hc:0 < c
H:a * c <= b
~ c == 0
auto with *.
Qed.

Lemma Qle_shift_inv_l : forall a c,
 0 < c -> a*c <= 1 -> a <= /c.forall a c : Q, 0 < c -> a * c <= 1 -> a <= / c
Proof.forall a c : Q, 0 < c -> a * c <= 1 -> a <= / c
intros a c Hc H.a, c:Q
Hc:0 < c
H:a * c <= 1
a <= / c
setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).a, c:Q
Hc:0 < c
H:a * c <= 1
a <= 1 * / c
change (a <= 1/c).a, c:Q
Hc:0 < c
H:a * c <= 1
a <= 1 / c
apply Qle_shift_div_l; assumption.
Qed.

Lemma Qle_shift_div_r : forall a b c,
 0 < b -> a <= c*b -> a/b <= c.forall a b c : Q, 0 < b -> a <= c * b -> a / b <= c
Proof.forall a b c : Q, 0 < b -> a <= c * b -> a / b <= c
intros a b c Hc H.a, b, c:Q
Hc:0 < b
H:a <= c * b
a / b <= c
apply Qmult_lt_0_le_reg_r with b.a, b, c:Q
Hc:0 < b
H:a <= c * b
0 < b
a, b, c:Q
Hc:0 < b
H:a <= c * b
a / b * b <= c * b
 assumption.a, b, c:Q
Hc:0 < b
H:a <= c * b
a / b * b <= c * b
setoid_replace (a/b*b) with (b*(a/b)) by apply Qmult_comm.a, b, c:Q
Hc:0 < b
H:a <= c * b
b * (a / b) <= c * b
rewrite Qmult_div_r; try assumption.a, b, c:Q
Hc:0 < b
H:a <= c * b
~ b == 0
auto with *.
Qed.

Lemma Qle_shift_inv_r : forall b c,
 0 < b -> 1 <= c*b -> /b <= c.forall b c : Q, 0 < b -> 1 <= c * b -> / b <= c
Proof.forall b c : Q, 0 < b -> 1 <= c * b -> / b <= c
intros b c Hc H.b, c:Q
Hc:0 < b
H:1 <= c * b
/ b <= c
setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).b, c:Q
Hc:0 < b
H:1 <= c * b
1 * / b <= c
change (1/b <= c).b, c:Q
Hc:0 < b
H:1 <= c * b
1 / b <= c
apply Qle_shift_div_r; assumption.
Qed.

Lemma Qinv_lt_0_compat : forall a, 0 < a -> 0 < /a.forall a : Q, 0 < a -> 0 < / a
Proof.forall a : Q, 0 < a -> 0 < / a
intros [[|n|n] d] Ha; assumption.
Qed.

Lemma Qlt_shift_div_l : forall a b c,
 0 < c -> a*c < b -> a < b/c.forall a b c : Q, 0 < c -> a * c < b -> a < b / c
Proof.forall a b c : Q, 0 < c -> a * c < b -> a < b / c
intros a b c Hc H.a, b, c:Q
Hc:0 < c
H:a * c < b
a < b / c
apply Qnot_le_lt.a, b, c:Q
Hc:0 < c
H:a * c < b
~ b / c <= a
intros H0.a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
False
apply (Qlt_not_le _ _ H).a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
b <= a * c
apply Qmult_lt_0_le_reg_r with (/c).a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
0 < / c
a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
b * / c <= a * c * / c
 apply Qinv_lt_0_compat.a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
0 < c
a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
b * / c <= a * c * / c
 assumption.a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
b * / c <= a * c * / c
setoid_replace (a*c/c) with (a) by (apply Qdiv_mult_l; auto with *).a, b, c:Q
Hc:0 < c
H:a * c < b
H0:b / c <= a
b * / c <= a
assumption.
Qed.

Lemma Qlt_shift_inv_l : forall a c,
 0 < c -> a*c < 1 -> a < /c.forall a c : Q, 0 < c -> a * c < 1 -> a < / c
Proof.forall a c : Q, 0 < c -> a * c < 1 -> a < / c
intros a c Hc H.a, c:Q
Hc:0 < c
H:a * c < 1
a < / c
setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).a, c:Q
Hc:0 < c
H:a * c < 1
a < 1 * / c
change (a < 1/c).a, c:Q
Hc:0 < c
H:a * c < 1
a < 1 / c
apply Qlt_shift_div_l; assumption.
Qed.

Lemma Qlt_shift_div_r : forall a b c,
 0 < b -> a < c*b -> a/b < c.forall a b c : Q, 0 < b -> a < c * b -> a / b < c
Proof.forall a b c : Q, 0 < b -> a < c * b -> a / b < c
intros a b c Hc H.a, b, c:Q
Hc:0 < b
H:a < c * b
a / b < c
apply Qnot_le_lt.a, b, c:Q
Hc:0 < b
H:a < c * b
~ c <= a / b
intros H0.a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
False
apply (Qlt_not_le _ _ H).a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
c * b <= a
apply Qmult_lt_0_le_reg_r with (/b).a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
0 < / b
a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
c * b * / b <= a * / b
 apply Qinv_lt_0_compat.a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
0 < b
a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
c * b * / b <= a * / b
 assumption.a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
c * b * / b <= a * / b
setoid_replace (c*b/b) with (c) by (apply Qdiv_mult_l; auto with *).a, b, c:Q
Hc:0 < b
H:a < c * b
H0:c <= a / b
c <= a * / b
assumption.
Qed.

Lemma Qlt_shift_inv_r : forall b c,
 0 < b -> 1 < c*b -> /b < c.forall b c : Q, 0 < b -> 1 < c * b -> / b < c
Proof.forall b c : Q, 0 < b -> 1 < c * b -> / b < c
intros b c Hc H.b, c:Q
Hc:0 < b
H:1 < c * b
/ b < c
setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).b, c:Q
Hc:0 < b
H:1 < c * b
1 * / b < c
change (1/b < c).b, c:Q
Hc:0 < b
H:1 < c * b
1 / b < c
apply Qlt_shift_div_r; assumption.
Qed.

Rational to the n-th power

Definition Qpower_positive : Q -> positive -> Q :=
 pow_pos Qmult.

Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive.Proper (Qeq ==> eq ==> Qeq) Qpower_positive
Proof.Proper (Qeq ==> eq ==> Qeq) Qpower_positive
intros x x' Hx y y' Hy.x, x':Q
Hx:x == x'
y, y':positive
Hy:y = y'
Qpower_positive x y == Qpower_positive x' y' rewrite <-Hy; clear y' Hy.x, x':Q
Hx:x == x'
y:positive
Qpower_positive x y == Qpower_positive x' y
unfold Qpower_positive.x, x':Q
Hx:x == x'
y:positive
pow_pos Qmult x y == pow_pos Qmult x' y
induction y; simpl;
try rewrite IHy;
try rewrite Hx;
reflexivity.
Qed.

Definition Qpower (q:Q) (z:Z) :=
    match z with
      | Zpos p => Qpower_positive q p
      | Z0 => 1
      | Zneg p => /Qpower_positive q p
    end.

Notation " q ^ z " := (Qpower q z) : Q_scope.

Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower.Proper (Qeq ==> eq ==> Qeq) Qpower
Proof.Proper (Qeq ==> eq ==> Qeq) Qpower
intros x x' Hx y y' Hy.x, x':Q
Hx:x == x'
y, y':Z
Hy:y = y'
x ^ y == x' ^ y' rewrite <- Hy; clear y' Hy.x, x':Q
Hx:x == x'
y:Z
x ^ y == x' ^ y
destruct y; simpl; rewrite ?Hx; auto with *.
Qed.