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.