# Library comparison

``` Require Import ZArith. Require Import QArith. Require Import misc. Require Import Q_misc. Require Import floor. Coercion Local Z_of_nat : nat >-> Z. Property Zlt_impl_Zle:   forall x y: Z,    (x < y + 1%nat)%Z -> (x <= y)%Z. Proof.   intros.   apply Zle_left_rev.   replace (y + - x)%Z with ((y + 1) + -1 + - x)%Z; try omega.   apply Zlt_left.   auto. Qed. Property Zle_impl_Zlt:   forall x y: Z,    (x <= y)%Z -> (x < y + 1)%Z. Proof.   intros.   apply (Zle_lt_trans x y (y + 1)%Z); auto with zarith. Qed. Property Zgt_impl_Zge:   forall (x: nat) (y: Z),    (x+1%nat > y )%Z -> (x >= y)%Z. Proof.   intros x y H_cmp.   apply Zle_ge.   apply Zgt_lt in H_cmp.   apply Zlt_impl_Zle.   assumption. Qed. 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. ```