Library comparison

Require Import ZArith.
Require Import QArith.
Require Import misc.
Require Import Z_misc.
Require Import Q_misc.
Require Import floor.

Coercion Local Z_of_nat : nat >-> Z.

Property Qle_impl_Qlt:
forall x y epsilon : Q,
forall H_epsilon: epsilon > 0,
x <= y -> x < y + epsilon.
Proof.
intros x y epsilon H_epsilon H_le.
apply (Qle_lt_trans x (y + 0) (y + epsilon)); try solve [ring_simplify; auto].
apply Qplus_lt_compat_l.
assumption.
Qed.

Property Qlt_impl_Qle_aux:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon = 1 # Qden y,
x < y -> x <= y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply (Qle_trans
x
(fl (y - epsilon))
(y - epsilon));
try solve [ elim (fl_def (y - epsilon)); auto].
apply Zle_impl_Qle.
apply Zlt_impl_Zle.
rewrite <- Zopp_involutive.
assert (H_aux:
(- - (fl (y - epsilon) + 1%nat))%Z = (- (- fl (y - epsilon) - 1))%Z).
ring.
rewrite H_aux; clear H_aux.
rewrite H_epsilon.
rewrite <- fl_m_n.
fold (cg y).
apply Qlt_impl_Zlt.
apply (Qlt_le_trans x y (cg y)); auto.
elim (cg_def_linear y); auto.
Qed.

Property Qlt_impl_Qle:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon <= 1 # Qden y,
x < y -> x <= y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply (Qle_trans
x
(y - (1 # Qden y))
(y - epsilon)).
apply Qlt_impl_Qle_aux; auto.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply Qopp_le_compat.
assumption.
Qed.

Property Qlt_impl_Qle_red:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon <= 1 # Qden (Qred y),
x < y -> x <= Qred y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply Qlt_impl_Qle; auto.
rewrite Qred_correct.
assumption.
Qed.