Qreals.v

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 Rbase.
Require Export QArith_base.

Injection of rational numbers into real numbers.

Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.

Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.forall p : positive, IZR (Z.pos p) <> 0%R
Proof.forall p : positive, IZR (Z.pos p) <> 0%R
intros.p:positive
IZR (Z.pos p) <> 0%R
now apply not_O_IZR.
Qed.

Hint Resolve IZR_nz Rmult_integral_contrapositive : core.

Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.forall x y : Q, Q2R x = Q2R y -> x == y
Proof.forall x y : Q, Q2R x = Q2R y -> x == y
unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2))%R =
(IZR y1 * / IZR (Z.pos y2))%R
(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
apply eq_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2))%R =
(IZR y1 * / IZR (Z.pos y2))%R
IZR (x1 * Z.pos y2) = IZR (y1 * Z.pos x2)
do 2 rewrite mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2))%R =
(IZR y1 * / IZR (Z.pos y2))%R
(IZR x1 * IZR (Z.pos y2))%R =
(IZR y1 * IZR (Z.pos x2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
H:(X1 * / X2)%R = (IZR y1 * / IZR (Z.pos y2))%R
X2nz:X2 <> 0%R
(X1 * IZR (Z.pos y2))%R = (IZR y1 * X2)%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2)%R = (Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * Y2)%R = (Y1 * X2)%R
assert ((X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2)%R = (Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R
x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2)%R = (Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
H0:(X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R
(X1 * Y2)%R = (Y1 * X2)%R
rewrite <- H; field; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2)%R = (Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
H0:(X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R
(X1 * Y2)%R = (Y1 * X2)%R
rewrite Rinv_r_simpl_m in H0; auto; rewrite H0; field; auto.
Qed.

Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y.forall x y : Q, x == y -> Q2R x = Q2R y
Proof.forall x y : Q, x == y -> Q2R x = Q2R y
unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
(IZR x1 * / IZR (Z.pos x2))%R =
(IZR y1 * / IZR (Z.pos y2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
(X1 * / X2)%R = (IZR y1 * / IZR (Z.pos y2))%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * / X2)%R = (Y1 * / Y2)%R
assert ((X1 * Y2)%R = (Y1 * X2)%R).x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * Y2)%R = (Y1 * X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2)%R = (Y1 * X2)%R
(X1 * / X2)%R = (Y1 * / Y2)%R
 unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
IZR (x1 * Z.pos y2) = IZR (y1 * Z.pos x2)
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2)%R = (Y1 * X2)%R
(X1 * / X2)%R = (Y1 * / Y2)%R
 apply IZR_eq; auto.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2)%Z = (y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2)%R = (Y1 * X2)%R
(X1 * / X2)%R = (Y1 * / Y2)%R
clear H.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2)%R = (Y1 * X2)%R
(X1 * / X2)%R = (Y1 * / Y2)%R
field_simplify_eq; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2)%R = (Y1 * X2)%R
(X1 * Y2)%R = (X2 * Y1)%R
rewrite H0; ring.
Qed.

Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.forall x y : Q, (Q2R x <= Q2R y)%R -> x <= y
Proof.forall x y : Q, (Q2R x <= Q2R y)%R -> x <= y
unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <=
 IZR y1 * / IZR (Z.pos y2))%R
(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
apply le_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <=
 IZR y1 * / IZR (Z.pos y2))%R
(IZR (x1 * Z.pos y2) <= IZR (y1 * Z.pos x2))%R
do 2 rewrite mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <=
 IZR y1 * / IZR (Z.pos y2))%R
(IZR x1 * IZR (Z.pos y2) <= IZR y1 * IZR (Z.pos x2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
H:(X1 * / X2 <= IZR y1 * / IZR (Z.pos y2))%R
X2nz:X2 <> 0%R
(X1 * IZR (Z.pos y2) <= IZR y1 * X2)%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * Y2 <= Y1 * X2)%R
replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * / X2 * (X2 * Y2) <= Y1 * X2)%R
replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * / X2 * (X2 * Y2) <= Y1 * / Y2 * (X2 * Y2))%R
apply Rmult_le_compat_r; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 <= X2 * Y2)%R
apply Rmult_le_pos.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 <= X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 <= Y2)%R
now apply IZR_le.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 <= Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 <= Y2)%R
now apply IZR_le.
Qed.

Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R.forall x y : Q, x <= y -> (Q2R x <= Q2R y)%R
Proof.forall x y : Q, x <= y -> (Q2R x <= Q2R y)%R
unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
(IZR x1 * / IZR (Z.pos x2) <=
 IZR y1 * / IZR (Z.pos y2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
(X1 * / X2 <= IZR y1 * / IZR (Z.pos y2))%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * / X2 <= Y1 * / Y2)%R
assert (X1 * Y2 <= Y1 * X2)%R.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * Y2 <= Y1 * X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * / X2 <= Y1 * / Y2)%R
 unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(IZR (x1 * Z.pos y2) <= IZR (y1 * Z.pos x2))%R
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * / X2 <= Y1 * / Y2)%R
 apply IZR_le; auto.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 <= y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * / X2 <= Y1 * / Y2)%R
clear H.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * / X2 <= Y1 * / Y2)%R
replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * Y2 * (/ X2 * / Y2) <= Y1 * / Y2)%R
replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(X1 * Y2 * (/ X2 * / Y2) <= Y1 * X2 * (/ X2 * / Y2))%R
apply Rmult_le_compat_r; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(0 <= / X2 * / Y2)%R
apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(0 < X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(0 < Y2)%R
now apply IZR_lt.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 <= Y1 * X2)%R
(0 < Y2)%R
now apply IZR_lt.
Qed.

Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.forall x y : Q, (Q2R x < Q2R y)%R -> x < y
Proof.forall x y : Q, (Q2R x < Q2R y)%R -> x < y
unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <
 IZR y1 * / IZR (Z.pos y2))%R
(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
apply lt_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <
 IZR y1 * / IZR (Z.pos y2))%R
(IZR (x1 * Z.pos y2) < IZR (y1 * Z.pos x2))%R
do 2 rewrite mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(IZR x1 * / IZR (Z.pos x2) <
 IZR y1 * / IZR (Z.pos y2))%R
(IZR x1 * IZR (Z.pos y2) < IZR y1 * IZR (Z.pos x2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
H:(X1 * / X2 < IZR y1 * / IZR (Z.pos y2))%R
X2nz:X2 <> 0%R
(X1 * IZR (Z.pos y2) < IZR y1 * X2)%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * Y2 < Y1 * X2)%R
replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * / X2 * (X2 * Y2) < Y1 * X2)%R
replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(X1 * / X2 * (X2 * Y2) < Y1 * / Y2 * (X2 * Y2))%R
apply Rmult_lt_compat_r; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 < X2 * Y2)%R
apply Rmult_lt_0_compat.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 < X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 < Y2)%R
now apply IZR_lt.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
H:(X1 * / X2 < Y1 * / Y2)%R
X2nz:X2 <> 0%R
Y2nz:Y2 <> 0%R
(0 < Y2)%R
now apply IZR_lt.
Qed.

Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R.forall x y : Q, x < y -> (Q2R x < Q2R y)%R
Proof.forall x y : Q, x < y -> (Q2R x < Q2R y)%R
unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden;
 intros.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
(IZR x1 * / IZR (Z.pos x2) < IZR y1 * / IZR (Z.pos y2))%R
set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2);
 set (X2 := IZR (Zpos x2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
(X1 * / X2 < IZR y1 * / IZR (Z.pos y2))%R
set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
 set (Y2 := IZR (Zpos y2)) in *.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * / X2 < Y1 * / Y2)%R
assert (X1 * Y2 < Y1 * X2)%R.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(X1 * Y2 < Y1 * X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * / X2 < Y1 * / Y2)%R
 unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
(IZR (x1 * Z.pos y2) < IZR (y1 * Z.pos x2))%R
x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * / X2 < Y1 * / Y2)%R
 apply IZR_lt; auto.x1:Z
x2:positive
y1:Z
y2:positive
H:(x1 * Z.pos y2 < y1 * Z.pos x2)%Z
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * / X2 < Y1 * / Y2)%R
clear H.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * / X2 < Y1 * / Y2)%R
replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * Y2 * (/ X2 * / Y2) < Y1 * / Y2)%R
replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(X1 * Y2 * (/ X2 * / Y2) < Y1 * X2 * (/ X2 * / Y2))%R
apply Rmult_lt_compat_r; auto.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(0 < / X2 * / Y2)%R
apply Rmult_lt_0_compat; apply Rinv_0_lt_compat.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(0 < X2)%R
x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(0 < Y2)%R
now apply IZR_lt.x1:Z
x2:positive
y1:Z
y2:positive
X1:=IZR x1:R
X2:=IZR (Z.pos x2):R
X2nz:X2 <> 0%R
Y1:=IZR y1:R
Y2:=IZR (Z.pos y2):R
Y2nz:Y2 <> 0%R
H0:(X1 * Y2 < Y1 * X2)%R
(0 < Y2)%R
now apply IZR_lt.
Qed.

Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.forall x y : Q, Q2R (x + y) = (Q2R x + Q2R y)%R
Proof.forall x y : Q, Q2R (x + y) = (Q2R x + Q2R y)%R
unfold Qplus, Qeq, Q2R; intros (x1, x2) (y1, y2);
 unfold Qden, Qnum.x1:Z
x2:positive
y1:Z
y2:positive
(IZR (x1 * Z.pos y2 + y1 * Z.pos x2) *
 / IZR (Z.pos (x2 * y2)))%R =
(IZR x1 * / IZR (Z.pos x2) + IZR y1 * / IZR (Z.pos y2))%R
simpl_mult.x1:Z
x2:positive
y1:Z
y2:positive
(IZR (x1 * Z.pos y2 + y1 * Z.pos x2) *
 / IZR (Z.pos x2 * Z.pos y2))%R =
(IZR x1 * / IZR (Z.pos x2) + IZR y1 * / IZR (Z.pos y2))%R
rewrite plus_IZR.x1:Z
x2:positive
y1:Z
y2:positive
((IZR (x1 * Z.pos y2) + IZR (y1 * Z.pos x2)) *
 / IZR (Z.pos x2 * Z.pos y2))%R =
(IZR x1 * / IZR (Z.pos x2) + IZR y1 * / IZR (Z.pos y2))%R
do 3 rewrite mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
((IZR x1 * IZR (Z.pos y2) + IZR y1 * IZR (Z.pos x2)) *
 / (IZR (Z.pos x2) * IZR (Z.pos y2)))%R =
(IZR x1 * / IZR (Z.pos x2) + IZR y1 * / IZR (Z.pos y2))%R
field; auto.
Qed.

Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R.forall x y : Q, Q2R (x * y) = (Q2R x * Q2R y)%R
Proof.forall x y : Q, Q2R (x * y) = (Q2R x * Q2R y)%R
unfold Qmult, Qeq, Q2R; intros (x1, x2) (y1, y2);
 unfold Qden, Qnum.x1:Z
x2:positive
y1:Z
y2:positive
(IZR (x1 * y1) * / IZR (Z.pos (x2 * y2)))%R =
(IZR x1 * / IZR (Z.pos x2) *
 (IZR y1 * / IZR (Z.pos y2)))%R
simpl_mult.x1:Z
x2:positive
y1:Z
y2:positive
(IZR (x1 * y1) * / IZR (Z.pos x2 * Z.pos y2))%R =
(IZR x1 * / IZR (Z.pos x2) *
 (IZR y1 * / IZR (Z.pos y2)))%R
do 2 rewrite mult_IZR.x1:Z
x2:positive
y1:Z
y2:positive
(IZR x1 * IZR y1 * / (IZR (Z.pos x2) * IZR (Z.pos y2)))%R =
(IZR x1 * / IZR (Z.pos x2) *
 (IZR y1 * / IZR (Z.pos y2)))%R
field; auto.
Qed.

Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R.forall x : Q, Q2R (- x) = (- Q2R x)%R
Proof.forall x : Q, Q2R (- x) = (- Q2R x)%R
unfold Qopp, Qeq, Q2R; intros (x1, x2); unfold Qden, Qnum.x1:Z
x2:positive
(IZR (- x1) * / IZR (Z.pos x2))%R =
(- (IZR x1 * / IZR (Z.pos x2)))%R
rewrite Ropp_Ropp_IZR.x1:Z
x2:positive
(- IZR x1 * / IZR (Z.pos x2))%R =
(- (IZR x1 * / IZR (Z.pos x2)))%R
field; auto.
Qed.

Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R.forall x y : Q, Q2R (x - y) = (Q2R x - Q2R y)%R
Proof.forall x y : Q, Q2R (x - y) = (Q2R x - Q2R y)%R
unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto.
Qed.

Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R.forall x : Q, ~ x == 0 -> Q2R (/ x) = (/ Q2R x)%R
Proof.forall x : Q, ~ x == 0 -> Q2R (/ x) = (/ Q2R x)%R
unfold Qinv, Q2R, Qeq; intros (x1, x2).x1:Z
x2:positive
(Qnum (x1 # x2) * QDen 0)%Z <>
(Qnum 0 * QDen (x1 # x2))%Z ->
(IZR
   (Qnum
      match Qnum (x1 # x2) with
      | 0%Z => 0
      | Z.pos p => QDen (x1 # x2) # p
      | Z.neg p => Z.neg (Qden (x1 # x2)) # p
      end) *
 /
 IZR
   (QDen
      match Qnum (x1 # x2) with
      | 0%Z => 0
      | Z.pos p => QDen (x1 # x2) # p
      | Z.neg p => Z.neg (Qden (x1 # x2)) # p
      end))%R =
(/ (IZR (Qnum (x1 # x2)) * / IZR (QDen (x1 # x2))))%R case x1; unfold Qnum, Qden.x1:Z
x2:positive
(0 * 1)%Z <> (0 * Z.pos x2)%Z ->
(0 * / 1)%R = (/ (0 * / IZR (Z.pos x2)))%R
x1:Z
x2:positive
forall p : positive,
(Z.pos p * 1)%Z <> (0 * Z.pos x2)%Z ->
(IZR (Z.pos x2) * / IZR (Z.pos p))%R =
(/ (IZR (Z.pos p) * / IZR (Z.pos x2)))%R
x1:Z
x2:positive
forall p : positive,
(Z.neg p * 1)%Z <> (0 * Z.pos x2)%Z ->
(IZR (Z.neg x2) * / IZR (Z.pos p))%R =
(/ (IZR (Z.neg p) * / IZR (Z.pos x2)))%R
simpl; intros; elim H; trivial.x1:Z
x2:positive
forall p : positive,
(Z.pos p * 1)%Z <> (0 * Z.pos x2)%Z ->
(IZR (Z.pos x2) * / IZR (Z.pos p))%R =
(/ (IZR (Z.pos p) * / IZR (Z.pos x2)))%R
x1:Z
x2:positive
forall p : positive,
(Z.neg p * 1)%Z <> (0 * Z.pos x2)%Z ->
(IZR (Z.neg x2) * / IZR (Z.pos p))%R =
(/ (IZR (Z.neg p) * / IZR (Z.pos x2)))%R
intros; field; auto.x1:Z
x2:positive
forall p : positive,
(Z.neg p * 1)%Z <> (0 * Z.pos x2)%Z ->
(IZR (Z.neg x2) * / IZR (Z.pos p))%R =
(/ (IZR (Z.neg p) * / IZR (Z.pos x2)))%R 
intros;
  change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R;
  change (IZR (Zneg p)) with (- IZR (Zpos p))%R;
  simpl; field; (*auto 8 with real.*)
  repeat split; auto; auto with real.
Qed.

Lemma Q2R_div :
 forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R.forall x y : Q,
~ y == 0 -> Q2R (x / y) = (Q2R x / Q2R y)%R
Proof.forall x y : Q,
~ y == 0 -> Q2R (x / y) = (Q2R x / Q2R y)%R
unfold Qdiv, Rdiv.forall x y : Q,
~ y == 0 -> Q2R (x * / y) = (Q2R x * / Q2R y)%R
intros; rewrite Q2R_mult.x, y:Q
H:~ y == 0
(Q2R x * Q2R (/ y))%R = (Q2R x * / Q2R y)%R
rewrite Q2R_inv; auto.
Qed.

Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.