Library Stdlib.QArith.QArith_base


From Stdlib Require Export BinInt.
From Stdlib Require Export ZArithRing.
From Stdlib Require Export ZArith.BinInt.
From Stdlib Require Export Morphisms Setoid Bool.

From Stdlib Require ZArith.Zcompare.
From Stdlib Require ZArith_dec.

Definition of Q and basic properties

Rationals are pairs of Z and positive numbers.

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

Declare Scope hex_Q_scope.
Delimit Scope hex_Q_scope with xQ.

Declare Scope Q_scope.
Delimit Scope Q_scope with Q.
Bind Scope Q_scope with Q.
Arguments Qmake _%_Z _%_positive.

Register Q as rat.Q.type.
Register Qmake as rat.Q.Qmake.

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 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.
Notation "x <= y < z" := (x<=y/\y<z) : Q_scope.
Notation "x < y <= z" := (x<y/\y<=z) : Q_scope.
Notation "x < y < z" := (x<y/\y<z) : Q_scope.

Register Qeq as rat.Q.Qeq.
Register Qle as rat.Q.Qle.
Register Qlt as rat.Q.Qlt.

Qeq construction from parts. Establishing equality by establishing equality for numerator and denominator separately.

Lemma Qden_cancel : forall (a b : Z) (p : positive),
  (a#p)==(b#p) -> a=b.

Lemma Qnum_cancel : forall (a b : positive) (z : Z),
  z<>0%Z -> (z#a)==(z#b) -> a=b.

injection from Z is injective.

Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.

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.

Lemma Qlt_alt p q : (p<q) <-> (p?=q = Lt).

Lemma Qgt_alt p q : (p>q) <-> (p?=q = Gt).

Lemma Qle_alt p q : (p<=q) <-> (p?=q <> Gt).

Lemma Qge_alt p q : (p>=q) <-> (p?=q <> Lt).

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

Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x).

Lemma Qcompare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x ?= y).

Properties of equality.


Theorem Qeq_refl x : x == x.

Theorem Qeq_sym x y : x == y -> y == x.

Theorem Qeq_trans x y z : x == y -> y == z -> x == z.

#[global]
Hint Immediate Qeq_sym : qarith.
#[global]
Hint Resolve Qeq_refl Qeq_trans : qarith.

In a word, Qeq is a setoid equality.

#[global]
Instance Q_Setoid : Equivalence Qeq.

Furthermore, this equality is decidable:

Theorem Qeq_dec x y : {x==y} + {~ x==y}.

Definition Qeq_bool x y :=
  (Z.eqb (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.

Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y.

Lemma Qeq_eq_bool x y : x == y -> Qeq_bool x y = true.

Lemma Qeq_bool_neq x y : Qeq_bool x y = false -> ~ x == y.

Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y.

Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y.

Theorem Qnot_eq_sym x y : ~x == y -> ~y == x.

Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.

Lemma Qeq_bool_refl x: Qeq_bool x x = true.

Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.

Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.

#[global]
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#1
  | 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.

Register Qplus as rat.Q.Qplus.
Register Qminus as rat.Q.Qminus.
Register Qopp as rat.Q.Qopp.
Register Qmult as rat.Q.Qmult.

Number notation for constants

Inductive IZ :=
  | IZpow_pos : Z -> positive -> IZ
  | IZ0 : IZ
  | IZpos : positive -> IZ
  | IZneg : positive -> IZ.

Inductive IQ :=
  | IQmake : IZ -> positive -> IQ
  | IQmult : IQ -> IQ -> IQ
  | IQdiv : IQ -> IQ -> IQ.

Definition IZ_of_Z z :=
  match z with
  | Z0 => IZ0
  | Zpos e => IZpos e
  | Zneg e => IZneg e
  end.

Definition IZ_to_Z z :=
  match z with
  | IZ0 => Some Z0
  | IZpos e => Some (Zpos e)
  | IZneg e => Some (Zneg e)
  | IZpow_pos _ _ => None
  end.

Definition of_decimal (d:Decimal.decimal) : IQ :=
  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 den := Nat.iter (Decimal.nb_digits f) (Pos.mul 10) 1%positive in
  let q := IQmake (IZ_of_Z num) den in
  let e := Z.of_int e in
  match e with
  | Z0 => q
  | Zpos e => IQmult q (IQmake (IZpow_pos 10 e) 1)
  | Zneg e => IQdiv q (IQmake (IZpow_pos 10 e) 1)
  end.

Definition IQmake_to_decimal num den :=
  let num := Z.to_int num in
  let (den, e_den) := Decimal.nztail (Pos.to_uint den) in
  match den with
  | Decimal.D1 Decimal.Nil =>
    match e_den with
    | O => Some (Decimal.Decimal num Decimal.Nil)
    | ne =>
      let ai := Decimal.abs num in
      let ni := Decimal.nb_digits ai in
      if Nat.ltb ne ni then
        let i := Decimal.del_tail_int ne num in
        let f := Decimal.del_head (Nat.sub ni ne) ai in
        Some (Decimal.Decimal i f)
      else
        let z := match num with
          | Decimal.Pos _ => Decimal.Pos (Decimal.zero)
          | Decimal.Neg _ => Decimal.Neg (Decimal.zero) end in
        Some (Decimal.Decimal z (Nat.iter (Nat.sub ne ni) Decimal.D0 ai))
    end
  | _ => None
  end.

Definition IQmake_to_decimal' num den :=
  match IZ_to_Z num with
  | None => None
  | Some num => IQmake_to_decimal num den
  end.

Definition to_decimal (n : IQ) : option Decimal.decimal :=
  match n with
  | IQmake num den => IQmake_to_decimal' num den
  | IQmult (IQmake num den) (IQmake (IZpow_pos 10 e) 1) =>
    match IQmake_to_decimal' num den with
    | Some (Decimal.Decimal i f) =>
      Some (Decimal.DecimalExp i f (Pos.to_int e))
    | _ => None
    end
  | IQdiv (IQmake num den) (IQmake (IZpow_pos 10 e) 1) =>
    match IQmake_to_decimal' num den with
    | Some (Decimal.Decimal i f) =>
      Some (Decimal.DecimalExp i f (Decimal.Neg (Pos.to_uint e)))
    | _ => None
    end
  | _ => None
  end.

Definition of_hexadecimal (d:Hexadecimal.hexadecimal) : IQ :=
  let '(i, f, e) :=
    match d with
    | Hexadecimal.Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil)
    | Hexadecimal.HexadecimalExp i f e => (i, f, e)
    end in
  let num := Z.of_hex_int (Hexadecimal.app_int i f) in
  let den := Nat.iter (Hexadecimal.nb_digits f) (Pos.mul 16) 1%positive in
  let q := IQmake (IZ_of_Z num) den in
  let e := Z.of_int e in
  match e with
  | Z0 => q
  | Zpos e => IQmult q (IQmake (IZpow_pos 2 e) 1)
  | Zneg e => IQdiv q (IQmake (IZpow_pos 2 e) 1)
  end.

Definition IQmake_to_hexadecimal num den :=
  let num := Z.to_hex_int num in
  let (den, e_den) := Hexadecimal.nztail (Pos.to_hex_uint den) in
  match den with
  | Hexadecimal.D1 Hexadecimal.Nil =>
    match e_den with
    | O => Some (Hexadecimal.Hexadecimal num Hexadecimal.Nil)
    | ne =>
      let ai := Hexadecimal.abs num in
      let ni := Hexadecimal.nb_digits ai in
      if Nat.ltb ne ni then
        let i := Hexadecimal.del_tail_int ne num in
        let f := Hexadecimal.del_head (Nat.sub ni ne) ai in
        Some (Hexadecimal.Hexadecimal i f)
      else
        let z := match num with
          | Hexadecimal.Pos _ => Hexadecimal.Pos (Hexadecimal.zero)
          | Hexadecimal.Neg _ => Hexadecimal.Neg (Hexadecimal.zero) end in
        Some (Hexadecimal.Hexadecimal z (Nat.iter (Nat.sub ne ni) Hexadecimal.D0 ai))
    end
  | _ => None
  end.

Definition IQmake_to_hexadecimal' num den :=
  match IZ_to_Z num with
  | None => None
  | Some num => IQmake_to_hexadecimal num den
  end.

Definition to_hexadecimal (n : IQ) : option Hexadecimal.hexadecimal :=
  match n with
  | IQmake num den => IQmake_to_hexadecimal' num den
  | IQmult (IQmake num den) (IQmake (IZpow_pos 2 e) 1) =>
    match IQmake_to_hexadecimal' num den with
    | Some (Hexadecimal.Hexadecimal i f) =>
      Some (Hexadecimal.HexadecimalExp i f (Pos.to_int e))
    | _ => None
    end
  | IQdiv (IQmake num den) (IQmake (IZpow_pos 2 e) 1) =>
    match IQmake_to_hexadecimal' num den with
    | Some (Hexadecimal.Hexadecimal i f) =>
      Some (Hexadecimal.HexadecimalExp i f (Decimal.Neg (Pos.to_uint e)))
    | _ => None
    end
  | _ => None
  end.

Definition of_number (n : Number.number) : IQ :=
  match n with
  | Number.Decimal d => of_decimal d
  | Number.Hexadecimal h => of_hexadecimal h
  end.

Definition to_number (q:IQ) : option Number.number :=
  match to_decimal q with
  | None => None
  | Some q => Some (Number.Decimal q)
  end.

Definition to_hex_number q :=
  match to_hexadecimal q with
  | None => None
  | Some q => Some (Number.Hexadecimal q)
  end.

Number Notation Q of_number to_hex_number (via IQ
  mapping [Qmake => IQmake, Qmult => IQmult, Qdiv => IQdiv,
           Z.pow_pos => IZpow_pos, Z0 => IZ0, Zpos => IZpos, Zneg => IZneg])
  : hex_Q_scope.

Number Notation Q of_number to_number (via IQ
  mapping [Qmake => IQmake, Qmult => IQmult, Qdiv => IQdiv,
           Z.pow_pos => IZpow_pos, Z0 => IZ0, Zpos => IZpos, Zneg => IZneg])
  : Q_scope.

A light notation for Zpos

Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).

Setoid compatibility results


#[global]
Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Instance Qopp_comp : Proper (Qeq==>Qeq) Qopp.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Instance Qminus_comp : Proper (Qeq==>Qeq==>Qeq) Qminus.

#[global]
Instance Qmult_comp : Proper (Qeq==>Qeq==>Qeq) Qmult.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Instance Qdiv_comp : Proper (Qeq==>Qeq==>Qeq) Qdiv.

#[global]
Instance Qcompare_comp : Proper (Qeq==>Qeq==>eq) Qcompare.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle.

#[global]
Instance Qlt_compat : Proper (Qeq==>Qeq==>iff) Qlt.

#[global]
Instance Qeqb_comp : Proper (Qeq==>Qeq==>eq) Qeq_bool.

#[global]
Instance Qleb_comp : Proper (Qeq==>Qeq==>eq) Qle_bool.

0 and 1 are apart

Lemma Q_apart_0_1 : ~ 1 == 0.

Properties of Qadd

Addition is associative:

Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z.

0 is a neutral element for addition:

Lemma Qplus_0_l : forall x, 0+x == x.

Lemma Qplus_0_r : forall x, x+0 == x.

Commutativity of addition:

Theorem Qplus_comm : forall x y, x+y == y+x.

Properties of Qopp


Lemma Qopp_involutive : forall q, - -q == q.

Theorem Qplus_opp_r : forall q, q+(-q) == 0.

Injectivity of addition (uses theory about Qopp above):

Lemma Qplus_inj_r (x y z: Q):
  x + z == y + z <-> x == y.

Lemma Qplus_inj_l (x y z: Q):
  z + x == z + y <-> x == y.

Properties of Qmult

Multiplication is associative:

Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p.

multiplication and zero

Lemma Qmult_0_l : forall x , 0*x == 0.

Lemma Qmult_0_r : forall x , x*0 == 0.

1 is a neutral element for multiplication:

Lemma Qmult_1_l : forall n, 1*n == n.

Theorem Qmult_1_r : forall n, n*1==n.

Commutativity of multiplication

Theorem Qmult_comm : forall x y, x*y==y*x.

Distributivity over Qadd

Theorem Qmult_plus_distr_r : forall x y z, x*(y+z)==(x*y)+(x*z).

Theorem Qmult_plus_distr_l : forall x y z, (x+y)*z==(x*z)+(y*z).

Integrality

Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0.

Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.

inject_Z is a ring homomorphism:


Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y.

Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y.

Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x.

Inverse and division.


Lemma Qinv_involutive : forall q, (/ / q) == q.

Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.

Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.

Lemma Qinv_pos: forall (a b : positive),
  / (Z.pos b # a) == Z.pos a # b.

Lemma Qinv_neg: forall (a b : positive),
  / (Z.neg b # a) == Z.neg a # b.

Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.

Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.

Lemma Qinv_plus_distr : forall a b c, ((a # c) + (b # c) == (a+b) # c)%Q.

Lemma Qinv_minus_distr : forall a b c, (a # c) + - (b # c) == (a-b) # c.

Injectivity of Qmult (requires theory about Qinv above):

Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y).

Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y).

Reduction and construction of Q

Removal/introduction of common factor in both numerator and denominator.


Lemma Qreduce_l : forall (a : Z) (b z : positive),
  (Zpos z)*a # z*b == a#b.

Lemma Qreduce_r : forall (a : Z) (b z : positive),
  a*(Zpos z) # b*z == a#b.

Lemma Qreduce_num_l : forall (a b : positive),
  Z.pos a # a * b == (1 # b).

Lemma Qreduce_num_r : forall (a b : positive),
  Z.pos b # a * b == (1 # a).

Lemma Qreduce_den_l : forall (a : positive) (b : Z),
  Z.pos a * b # a == (b # 1).

Lemma Qreduce_den_r : forall (a : Z) (b : positive),
  a * Z.pos b # b == (a # 1).

Lemma Qreduce_den_inject_Z_l : forall (a : positive) (b : Z),
  (Z.pos a * b # a == inject_Z b)%Q.

Lemma Qreduce_den_inject_Z_r : forall (a : Z) (b : positive),
  a * Z.pos b # b == inject_Z a.

Lemma Qreduce_zero: forall (d : positive),
  (0#d == 0)%Q.

Construction of a new rational by multiplication with an integer or pure fraction

(or to be more precise multiplication with a rational of the form z/1 or 1/p)

Lemma Qmult_inject_Z_l : forall (a : Z) (b : positive) (z : Z),
  (inject_Z z) * (a#b) == z*a#b.

Lemma Qmult_inject_Z_r : forall (a : Z) (b : positive) (z : Z),
  (a#b) * inject_Z z == a*z#b.

Lemma Qmult_frac_l : forall (a:Z) (b c:positive), (a # (b * c)) == (1#b) * (a#c).

Lemma Qmult_frac_r : forall (a:Z) (b c:positive), (a # (b * c)) == (a#b) * (1#c).

Properties of order upon Q.


Lemma Qle_refl x : x<=x.

Lemma Qle_antisym x y : x<=y -> y<=x -> x==y.

Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
  Open Scope Z_scope.
  Close Scope Z_scope.

#[global]
Hint Resolve Qle_trans : qarith.

Lemma Qlt_irrefl x : ~x<x.

Lemma Qlt_not_eq x y : x<y -> ~ x==y.

Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y).

Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y).

Large = strict or equal

Lemma Qle_lteq x y : x<=y <-> x<y \/ x==y.

Lemma Qlt_leneq: forall p q : Q, p < q <-> p <= q /\ ~ (p == q).

Lemma Qlt_le_weak x y : x<y -> x<=y.

Qgt and Qge are just a notations, but one might not know this and search for these lemmas

Lemma Qgt_lt: forall p q : Q, p > q -> q < p.

Lemma Qlt_gt: forall p q : Q, p < q -> q > p.

Lemma Qge_le: forall p q : Q, p >= q -> q <= p.

Lemma Qle_ge: forall p q : Q, p <= q -> q >= p.

Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.

x<y iff ~(y<=x)

Lemma Qnot_lt_le x y : ~ x < y -> y <= x.

Lemma Qnot_le_lt x y : ~ x <= y -> y < x.

Lemma Qlt_not_le x y : x < y -> ~ y <= x.

Lemma Qle_not_lt x y : x <= y -> ~ y < x.

Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.

#[global]
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}.

Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}.

Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }.

Compatibility of addition with order


Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.

Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.

#[global]
Hint Resolve Qopp_le_compat Qopp_lt_compat : qarith.

Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.

Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.

Lemma Qplus_le_compat :
  forall x y z t, x<=y -> z<=t -> x+z <= y+t.
  Open Scope Z_scope.
    Close Scope Z_scope.

Lemma Qplus_lt_le_compat :
  forall x y z t, x<y -> z<=t -> x+z < y+t.
  Open Scope Z_scope.
    Close Scope Z_scope.

Lemma Qplus_le_l (x y z: Q): x + z <= y + z <-> x <= y.

Lemma Qplus_le_r (x y z: Q): z + x <= z + y <-> x <= y.

Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y.

Lemma Qplus_lt_r (x y z: Q): z + x < z + y <-> x < y.

Lemma Qplus_lt_compat : forall x y z t : Q,
  x < y -> z < t -> x + z < y + t.

Compatibility of multiplication with order.


Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y).

Lemma Qmult_le_l (x y z: Q): 0 < z -> (z*x <= z*y <-> x <= y).

Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y).
 Open Scope Z_scope.
   Close Scope Z_scope.

Lemma Qmult_lt_l (x y z: Q): 0 < z -> (z*x < z*y <-> x < y).

Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.

Lemma Qmult_lt_0_compat : forall a b : Q, 0 < a -> 0 < b -> 0 < a * b.

Lemma Qmult_le_1_compat: forall a b : Q, 1 <= a -> 1 <= b -> 1 <= a * b.

Lemma Qmult_lt_1_compat: forall a b : Q, 1 < a -> 1 < b -> 1 < a * b.

Lemma Qmult_lt_compat_nonneg: forall x y z t : Q, 0 <= x < y -> 0 <= z < t -> x * z < y * t.

Lemma Qmult_le_lt_compat_pos: forall x y z t : Q, 0 < x <= y -> 0 < z < t -> x * z < y * t.

Lemma Qmult_le_compat_nonneg: forall x y z t : Q, 0 <= x <= y -> 0 <= z <= t -> x * z <= y * t.

Compatibility of inversion and division with order


Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a.

Lemma Qle_shift_div_l : forall a b c,
 0 < c -> a*c <= b -> a <= b/c.

Lemma Qle_shift_inv_l : forall a c,
 0 < c -> a*c <= 1 -> a <= /c.

Lemma Qle_shift_div_r : forall a b c,
 0 < b -> a <= c*b -> a/b <= c.

Lemma Qle_shift_inv_r : forall b c,
 0 < b -> 1 <= c*b -> /b <= c.

Lemma Qinv_lt_0_compat : forall a, 0 < a -> 0 < /a.

Lemma Qlt_shift_div_l : forall a b c,
 0 < c -> a*c < b -> a < b/c.

Lemma Qlt_shift_inv_l : forall a c,
 0 < c -> a*c < 1 -> a < /c.

Lemma Qlt_shift_div_r : forall a b c,
 0 < b -> a < c*b -> a/b < c.

Lemma Qlt_shift_inv_r : forall b c,
 0 < b -> 1 < c*b -> /b < c.

Lemma Qinv_lt_contravar : forall a b : Q,
    0 < a -> 0 < b -> (a < b <-> /b < /a).

Rational to the n-th power


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

#[global]
Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive.

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.

Register Qpower as rat.Q.Qpower.

#[global]
Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower.