Library Q_misc



Set Implicit Arguments.

Require Import ZArith.
Require Import Znumtheory.
Require Import Z_misc.
Require Import QArith.
Require Import Decidable.
Require Import misc.

Definition Q_of_nat (n:nat) := (inject_Z (Z_of_nat n)).
Coercion Local Q_of_nat : nat >-> Q.
Coercion Local inject_Z : Z >-> Q.

Definition in_Z (x: Q) :=
  exists y:Z, x == inject_Z y.

Property nat_in_Z:
  forall n: nat,
  in_Z (Q_of_nat n).
Proof.
  intro.
  exists (Z_of_nat n).
  unfold Qeq, Q_of_nat.
  reflexivity.
Qed.

Property Qplus_in_Z_compat:
  forall q: Q,
  forall x: Z,
  in_Z q -> in_Z (q + x).
Proof.
  intros q x H_in_Z.
  unfold in_Z in *.
  elim H_in_Z.
  intros q' H_q'.
  exists (q' + x)%Z.
  rewrite H_q'.
  unfold Qeq, Q_of_nat, Qplus.
  simpl.
  repeat rewrite Zmult_1_r.
  reflexivity.
Qed.

Lemma n_plus_1_eq_S_n:
  forall n: nat, (n + 1)%Q = S n.
Proof.
  intro n.
  unfold Q_of_nat, inject_Z, Z_of_nat.
  destruct n; [reflexivity |].
  do 2 rewrite Zpos_P_of_succ_nat.
  rewrite inj_S.
  unfold Qplus; simpl; apply f_equal2; auto.
  ring.
Qed.

Theorem S_n_m_1_eq_n: forall n : nat, ((S n) - 1)%Q = n.
Proof.
  intros.
  rewrite <- n_plus_1_eq_S_n.
  unfold Q_of_nat, inject_Z, Z_of_nat.
  destruct n; [reflexivity |].
  rewrite Zpos_P_of_succ_nat.
  unfold Qminus;
  unfold Qplus; simpl.
  apply f_equal2; auto.
  ring.
Qed.

Lemma Zplus_eq_Qplus:
  forall x y: Z,
  ((x + y)%Z == x + y)%Q.
Proof.
  intros; unfold Qeq; simpl; omega.
Qed.

Lemma Qmult_lt_0_lt_reg_r : forall x y z, 0 < z -> x*z < y*z -> x < y.
Proof.
  intros (a1,a2) (b1,b2) (c1,c2); unfold Qlt; simpl.
  Open Scope Z_scope.
  simpl_mult.
  replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
  replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
  intros; apply Zmult_lt_reg_r with (c1*'c2); auto with zarith.
  ring_simplify in H.
  assert (0 = 0 * c1).
    compute.
    trivial.
  rewrite H1.
  replace (c1 * 'c2) with ('c2 * c1) by ring.
  eapply Zmult_lt_compat_r; auto.
  compute.
  trivial.
  Close Scope Z_scope.
Qed.

Lemma Qinv_pos_strict:
  forall x,
  forall H_x_pos: x > 0,
  0 < / x.
Proof.
  intros.
  apply Qmult_lt_0_lt_reg_r with x; auto.
  ring_simplify.
  rewrite Qmult_inv_r.
    unfold Q_of_nat, Qlt.
    simpl.
    auto with zarith.

    unfold Qlt in H_x_pos.
    simpl in H_x_pos.
    ring_simplify in H_x_pos.
    unfold Q_of_nat, Qeq.
    simpl.
    auto with zarith.
Qed.

Lemma Qinv_pos:
  forall x,
  forall H_x_pos: x > 0,
  0 <= / x.
Proof.
  intros.
  apply Qmult_lt_0_le_reg_r with x; auto.
  apply Qle_trans with 0; ring_simplify.
    apply Qle_refl.
  rewrite Qmult_comm.
  rewrite Qmult_inv_r.
    unfold Q_of_nat, Qle.
    simpl.
    auto with zarith arith.

    unfold Qlt in H_x_pos.
    simpl in H_x_pos.
    ring_simplify in H_x_pos.
    unfold Q_of_nat, Qeq.
    simpl.
    auto with zarith.
Qed.

Theorem Qinv_ge_inv:
  forall x,
  forall H_x: x >= 1,
  / x <= 1.
Proof.
  intros.
  simpl in H_x.
  assert (H_x_pos: x > 0).
    assert (0 < 1).
      unfold Q_of_nat, Qlt; simpl; auto with zarith.
    apply (Qlt_le_trans 0 1 x H H_x).
  apply (Qmult_lt_0_le_reg_r (/x) 1 x H_x_pos).
  ring_simplify.
  rewrite Qmult_comm.
  rewrite Qmult_inv_r.
  assumption.
  unfold Qlt in H_x_pos.
  unfold Qeq.
  auto with zarith.
Qed.

Theorem Qdiv_le_compat:
  forall x y z,
  forall H_z_pos: z > 0,
  forall H_x_le_y: x <= y,
  x / z <= y / z.
Proof.
  intros.
  unfold Qdiv.
  apply Qmult_le_compat_r; auto with qarith.
  eapply Qinv_pos.
  assumption.
Qed.

Theorem le_impl_Qle:
  forall (x:nat) (y: nat),
  forall H_nat: (x <= y)%nat,
    x <= y.
Proof.
  intros.
  unfold Q_of_nat, Qle.
  simpl.
  ring_simplify.
  auto with zarith arith.
Qed.

Theorem ge_impl_Qge:
  forall (x:nat) (y: nat),
  forall H_nat: (x >= y)%nat,
    x >= y.
Proof.
  intros.
  unfold Q_of_nat.
  unfold Qle.
  simpl.
  ring_simplify.
  auto with zarith arith.
Qed.

Theorem Qle_impl_le:
  forall (x:nat) (y: nat),
  forall H_Q: x <= y,
    (x <= y)%nat.
Proof.
  intros.
  unfold Q_of_nat, Qle in H_Q.
  simpl in H_Q.
  replace ((Z_of_nat x * 1)%Z) with ((Z_of_nat x)%Z) in H_Q by ring.
  replace ((Z_of_nat y * 1)%Z) with ((Z_of_nat y)%Z) in H_Q by ring.
  apply inj_le_rev.
  assumption.
Qed.

Theorem Zle_impl_Qle:
  forall (x:Z) (y: Z),
  forall H_Z: (x <= y)%Z,
    inject_Z x <= inject_Z y.
Proof.
  intros.
  unfold Q_of_nat, Qle.
  simpl.
  ring_simplify.
  auto with zarith arith.
Qed.

Theorem Qle_impl_Zle:
  forall (x:Z) (y: Z),
  forall H_Q: (x <= y)%Q,
    (x <= y)%Z.
Proof.
  intros.
  unfold Q_of_nat, Qle in H_Q.
  simpl in H_Q.
  ring_simplify in H_Q.
  auto with zarith arith.
Qed.

Theorem Qeq_impl_Zeq:
  forall (x:Z) (y: Z),
  forall H_Q: (x == y)%Q,
    (x = y)%Z.
Proof.
  intros.
  unfold Q_of_nat, Qeq in H_Q.
  simpl in H_Q.
  ring_simplify in H_Q.
  auto with zarith arith.
Qed.

Theorem lt_impl_Qlt:
  forall (x:nat) (y:nat),
  forall H_Z: (x < y)%nat,
    Q_of_nat x < Q_of_nat y.
Proof.
  intros.
  unfold Q_of_nat, Qlt.
  simpl.
  ring_simplify.
  auto with zarith arith.
Qed.

Theorem Zlt_impl_Qlt:
  forall (x:Z) (y: Z),
  forall H_Z: (x < y)%Z,
    inject_Z x < inject_Z y.
Proof.
  intros.
  unfold Q_of_nat, Qlt.
  simpl.
  ring_simplify.
  auto with zarith arith.
Qed.

Theorem Qlt_impl_Zlt:
  forall (x:Z) (y: Z),
  forall H_Q: inject_Z x < inject_Z y,
    (x < y)%Z.
Proof.
  intros.
  unfold Q_of_nat, Qlt in H_Q.
  simpl in H_Q.
  ring_simplify in H_Q.
  auto with zarith arith.
Qed.

Theorem Qlt_impl_lt:
  forall (x:nat) (y: nat),
  forall H_Q: Q_of_nat x < Q_of_nat y,
    (x < y)%nat.
Proof.
  intros.
  unfold Q_of_nat, Qlt in H_Q.
  simpl in H_Q.
  ring_simplify in H_Q.
  auto with zarith arith.
Qed.

Theorem le_impl_Zle:
  forall (x:nat) (y: nat),
  forall H_nat: (x <= y)%nat,
    (Z_of_nat x <= Z_of_nat y)%Z.
Proof.
  intros.
  apply inj_le.
  assumption.
Qed.

Theorem abs_le_compat:
  forall x y,
  forall a d r,
  forall H_r: r > 0,
  forall H_x_le_y: x <= y,
  forall H_a_le_x_m_d_div_r: a <= (x - d) / r,
  a <= (y - d) / r.
Proof.
  intros.
  simpl in H_a_le_x_m_d_div_r.
  eapply (Qle_trans a ((x - d) / r) ((y - d) / r)); auto.
  eapply Qdiv_le_compat; auto.
  unfold Qminus.
  eapply Qplus_le_compat; auto.
  eapply Qle_refl.
Qed.

Theorem abs_le_compat_prim:
  forall x y,
  forall a d r,
  forall H_r: r >= 0,
  forall H_x_le_y: x <= y,
  forall H_a_le_x_m_d_div_r: a <= (x - d) * r,
  a <= (y - d) * r.
Proof.
  intros.
  simpl in H_a_le_x_m_d_div_r.
  eapply (Qle_trans a ((x - d) * r) ((y - d) * r)); auto.
  eapply Qmult_le_compat_r; auto.
  unfold Qminus.
  eapply Qplus_le_compat; auto.
  eapply Qle_refl.
Qed.

Theorem Qplus_eq_compat:
  forall a b x y,
  forall H_a_eq_b: a == b,
  forall H_x_eq_y: x == y,
  a + x == b + y.
Proof.
  intros.
  rewrite H_x_eq_y.
  rewrite H_a_eq_b.
  apply Qeq_refl.
Qed.

Theorem Qplus_lt_compat_l:
  forall a x y,
  forall H_x_eq_y: x < y,
  a + x < a + y.
Proof.
  intros.
  apply <- Qlt_minus_iff.
  assert (H_aux: a + y + - (a + x) == y + - x).
    ring.
  rewrite H_aux; clear H_aux.
  apply -> Qlt_minus_iff.
  assumption.
Qed.

Theorem Qle_plus:
  forall a x y,
  forall H_x_le_y: a + x <= a + y,
  x <= y.
Proof.
  intros.
  assert (H_m_a_le_m_a: -a <= -a).
    apply Qle_refl.
  generalize (Qplus_le_compat (-a) (-a) (a+x) (a+y) H_m_a_le_m_a H_x_le_y).
  intro H_cc.
  ring_simplify in H_cc.
  exact H_cc.
Qed.

Theorem Qlt_plus:
  forall a x y,
  a + x < a + y <-> x < y.
Proof.
  intros.
  split.
    intros.
    apply <- Qlt_minus_iff.
    assert (H_aux: (y + - x) == ((a + y) + - (a + x))).
      ring.
    rewrite H_aux; clear H_aux.
    apply -> Qlt_minus_iff; assumption.
    intros.
    apply <- Qlt_minus_iff.
    assert (H_aux: (y + - x) == ((a + y) + - (a + x))).
      ring.
    rewrite <- H_aux; clear H_aux.
    apply -> Qlt_minus_iff; assumption.
Qed.

Lemma plus_impl_Qplus:
  forall x y: nat,
    (x + y)% nat == (x + y)%Q.
Proof.
  intros.
  induction x.
    simpl.
    rewrite Qplus_0_l.
    reflexivity.

    assert (H_aux: (S x + y = S (x + y))%nat);
      auto with arith.
    rewrite H_aux; clear H_aux.
    rewrite <- n_plus_1_eq_S_n.
    rewrite <- n_plus_1_eq_S_n.
    assert (H_aux: x + 1 + y == (x + y) + 1).
      ring.
    rewrite H_aux; clear H_aux.
    apply Qplus_eq_compat; auto.
    apply Qeq_refl.
Qed.

Lemma minus_impl_Qminus:
  forall x y: nat,
  forall H_x_le_y: (x <= y)%nat,
    (y - x)% nat == (y - x)%Q.
Proof.
  intros.
  induction x.
    unfold Q_of_nat, Qminus, Qeq, Qplus.
    simpl.
    ring_simplify.
    rewrite <- minus_n_O.
    trivial.

    assert (H_x'_le_y: (x <= y)%nat).
      apply le_Sn_le.
      assumption.
    rewrite <- n_plus_1_eq_S_n.
    assert (H_aux: y - (x + 1) == (y - 1) - x).
      ring.
    rewrite H_aux; clear H_aux.
   case_eq y.
     intro H_y.
     rewrite H_y in H_x_le_y.
     generalize (le_Sn_O x).
     congruence.

     intros y' H_y.
     assert (H_aux: S y' - 1 = y').
       eapply (S_n_m_1_eq_n y').
     rewrite H_aux; clear H_aux.
     simpl.
     unfold Q_of_nat, Qeq, Qminus, Qplus; simpl.
     ring_simplify.
     rewrite inj_minus1; auto.
     rewrite H_y in H_x_le_y.
     auto with arith.
Qed.

Theorem simply_1:
  forall d1 r1 d2 r2 i,
  forall H_r1_pos: r1 > 0,
  forall H_r2_pos: r2 > 0,
  ((i - d1) / r1 - d2) / r2 == (i - (d1 + d2 * r1)) / (r1 * r2).
Proof.
  intros.
  field.
  simpl in H_r1_pos.
  simpl in H_r2_pos.
  unfold Qlt in H_r1_pos.
  unfold Qlt in H_r2_pos.
  unfold Qeq.
  split; auto with zarith.
Qed.

Theorem simply_1_prim:
  forall d1 r1 d2 r2 i,
  forall H_r1_non_null: ~ r1 == 0,

  ((i - d1) * r1 - d2) * r2 == (i - (d1 + d2 / r1)) * (r1 * r2).
Proof.
  intros.
  field.
  assumption.
Qed.

Property QDen_Qred_def:
  forall x: Q,
  (QDen (Qred x) = Zdiv (QDen x) (Zgcd (Qnum x) (QDen x)))%Z.
Proof.
  intros.
  unfold Qred.
  destruct x.
  case_eq (Zggcd Qnum (Zpos Qden)).
  intros z [r1 r2] H_eq.
  rewrite <- Zggcd_gcd.
  simpl.
  rewrite H_eq.
  simpl.
  assert (H:= Zggcd_correct_divisors Qnum (Zpos Qden) ).
  rewrite H_eq in H; destruct H.
  rewrite H0.
  rewrite Zmult_comm.
  assert (0 < z)%Z.
    assert (H_gcd:= Zgcd_gt_0_r Qnum (Zpos Qden)).
    rewrite <- Zggcd_gcd in H_gcd.
    rewrite H_eq in H_gcd.
    simpl in H_gcd.
    apply H_gcd.
    compute.
    reflexivity.
  rewrite Z_div_mult_full.
  assert (0 < r2)%Z.
    assert (H_z:= Zsgn_Zmult z r2).
    rewrite <- H0 in H_z.
    simpl in H_z.
    rewrite <- Zsgn_pos in H1.
    rewrite H1 in H_z.
    rewrite Zmult_1_l in H_z.
    symmetry in H_z.
    rewrite Zsgn_pos in H_z.
    assumption.
    destruct r2; compute in H1; try discriminate; auto.
  intro abs.
  subst.
  exact (Zlt_irrefl 0 H1).
Qed.

Property QDen_Qred_x_le_QDen_x:
  forall x: Q,
  (QDen (Qred x) <= QDen x)%Z.
Proof.
  intros.
  rewrite QDen_Qred_def.
  assert ((0 < Zgcd (Qnum x) (' Qden x))%Z).
    apply Zgcd_gt_0_r.
    compute.
    reflexivity.
  apply Zdiv_le_upper_bound; auto with zarith.
  rewrite <- (Zmult_1_r (Zpos (Qden x))) at 1.
  apply Zmult_le_compat_l.
  2: (compute; intro; discriminate).
  omega.
Qed.

Property inv_Qden_x_le_inv_Qden_Qred_x:
  forall x: Q,
  (1 # Qden x <= 1 # Qden (Qred x)).
Proof.
  intros.
  unfold Qle, Qnum, Qden.
  fold (Qden x).
  fold (Qden (Qred x)).
  repeat rewrite Zmult_1_l.
  apply QDen_Qred_x_le_QDen_x.
Qed.

Definition Qmin (n m:Q) :=
  match n ?= m with
    | Eq | Lt => n
    | Gt => m
  end.

Lemma Qle_min_l:
  forall n m : Q, Qmin n m <= n.
Proof.
  intros.
  unfold Qmin.
  case_eq (n ?= m); try solve [ intros; apply Qle_refl ].
  rewrite <- Qgt_alt.
  apply Qlt_le_weak.
Qed.

Lemma Qle_min_r:
  forall n m : Q, Qmin n m <= m.
Proof.
  intros.
  unfold Qmin.
  case_eq (n ?= m); try solve [ intros; apply Qle_refl ].
    rewrite <- Qeq_alt.
    intro H_cmp; rewrite H_cmp; apply Qle_refl.
    rewrite <- Qlt_alt.
    apply Qlt_le_weak.
Qed.

Lemma Qmin_dec : forall n m:Q, {Qmin n m = n} + {Qmin n m = m}.
Proof.
  unfold Qmin in |- *; intros; elim (n ?= m); auto.
Qed.

Lemma Qmin_irreducible : forall n m:Q, Qmin n m = n \/ Qmin n m = m.
Proof.
  intros n m; destruct (Qmin_dec n m); [left|right]; trivial.
Qed.

Definition Qmax (m n:Q) :=
  match m ?= n with
    | Eq | Gt => m
    | Lt => n
  end.

Lemma Qle_max_l:
  forall n m : Q, n <= Qmax n m.
Proof.
  intros.
  unfold Qmax.
  case_eq (n ?= m); try solve [ intros; apply Qle_refl ].
  rewrite <- Qlt_alt.
  apply Qlt_le_weak.
Qed.

Lemma Qle_max_r:
  forall n m : Q, m <= Qmax n m.
Proof.
  intros.
  unfold Qmax.
  case_eq (n ?= m); try solve [ intros; apply Qle_refl ].
    rewrite <- Qeq_alt.
    intro H_cmp; rewrite H_cmp; apply Qle_refl.
    rewrite <- Qgt_alt.
    apply Qlt_le_weak.
Qed.

Lemma Qmax_dec : forall n m:Q, {Qmax n m = n} + {Qmax n m = m}.
Proof.
  unfold Qmax in |- *; intros; elim (n ?= m); auto.
Qed.

Lemma Qmax_irreducible : forall n m:Q, Qmax n m = n \/ Qmax n m = m.
Proof.
  intros n m; destruct (Qmax_dec n m); [left|right]; trivial.
Qed.

Lemma den_r_le_den_r_i_p_b:
  forall r: Q,
  forall i: nat,
  forall b: Q,
  forall H_wf_b: Qden b = Qden r,
  1 # Qden r <= 1 # Qden (Qred (r * i + b)).
Proof.
  intros.
  unfold Qle, Qnum, Qden.
  fold (Qden (Qred (r * i + b))).
  fold (Qden r).
  repeat rewrite Zmult_1_l.
  simpl.
  rewrite H_wf_b.
  rewrite Pmult_1_r.
  assert (H_aux:
    (Zplus
      (Zmult (Zmult (Qnum r) (Z_of_nat i)) (Zpos (Qden r)))
      (Zmult (Qnum b) (Zpos (Qden r))))
    =
    (Zmult
      (Zplus
        (Zmult (Qnum r) (Z_of_nat i))
        (Qnum b))
      (Zpos (Qden r)))).
    ring.
  rewrite H_aux; clear H_aux.

  case_eq (Zggcd ((Qnum r * (Z_of_nat i) + Qnum b) * ' Qden r) (' (Qden r * Qden r)));
  intros z [r1 r2] H_eq; simpl.
  pose (H:= Zgcd_is_gcd ((Qnum r * (Z_of_nat i) + Qnum b) * ' Qden r) (' (Qden r * Qden r))).
  rewrite <- Zggcd_gcd in H.
  rewrite H_eq in H; simpl in H.
  inversion_clear H.
  assert (H_z: ((Zpos (Qden r)) | z)%Z).
    apply H2.
    exists (Qnum r * (Z_of_nat i) + Qnum b)%Z; auto.
    exists (Zpos (Qden r))%Z; auto with zarith.
  assert (Zpos (Qden r) <= z)%Z.
    apply Zdivide_le; auto.
    compute; intros; discriminate.
    change (0 < fst (z, (r1, r2)))%Z; rewrite <- H_eq; rewrite Zggcd_gcd.
    apply Zgcd_gt_0_r.
    compute; reflexivity.
    match goal with
    | H_eq : (Zggcd ?X ?Y) = _ |- _ =>
      assert (Hcd := Zggcd_correct_divisors X Y); rewrite H_eq in Hcd;
        destruct Hcd as [_ Hcd]; revert Hcd H; clear; intros
    end.
    rewrite Zpos_mult_morphism in Hcd.
    assert (H_Qden_r: (0 < Zpos (Qden r))).
      compute; reflexivity.
    assert (H_cc:
      ((Zpos (Qden r) * Zpos (Qden r)) / (Zpos (Qden r)) >= (z * r2) / z)%Z).
      rewrite Hcd.
      apply Zdiv_le_denom; auto.

      rewrite <- Hcd.
      apply Zle_ge.
      replace 0%Z with (0 * Zpos (Qden r))%Z by omega.
      apply Zmult_le_compat_r; apply Zlt_le_weak; assumption.

      rewrite Z_div_mult_full in H_cc.
      rewrite Zmult_comm in H_cc.
      rewrite Z_div_mult_full in H_cc.
      rewrite Z2P_correct.
      apply Zge_le.
      assumption.

      apply -> Zsgn_pos.
      rewrite <- (Zmult_1_l (Zsgn r2)).
      assert (H_z: (Zsgn z = 1)%Z).
        apply <- Zsgn_pos.
        apply (Zlt_le_trans
          0
          (Zpos (Qden r))
          z); auto.
      rewrite <- H_z at 1.
      rewrite <- Zsgn_Zmult.
      rewrite <- Hcd.
      apply <- Zsgn_pos.
      replace 0%Z with (0 * Zpos (Qden r))%Z by omega.
      apply Zmult_lt_compat_r;
        try solve [ compute; reflexivity ].

      intro.
      symmetry in H0.
      absurd (0%Z = z); auto.
      apply Zlt_not_eq.
      apply (Zlt_le_trans
        0
        (Zpos (Qden r))
        z); auto.

      intro.
      symmetry in H0.
      absurd (0%Z = Zpos (Qden r)); auto.
      apply Zlt_not_eq.
      compute; reflexivity.
Qed.

Lemma den_r_i_p_b_le_den_r:
  forall r: Q,
  forall i: nat,
  forall b: Q,
  forall H_wf_b: Qden b = Qden r,
   1 # Qden (r * i + b) <= 1 # Qden r.
Proof.
  intros.
  unfold Qle, Qnum, Qden.
  fold (Qden (r * i + b)).
  fold (Qden r).
  repeat rewrite Zmult_1_l.
  simpl.
  rewrite H_wf_b.
  rewrite Pmult_1_r.
  rewrite <- (Pmult_1_r (Qden r)) at 1.
  repeat rewrite Zpos_mult_morphism.
  apply Zmult_le_compat_l.
    apply Zlt_impl_Zle.
    assert (H_aux: (Zpos xH) = (0 + 1)%Z).
      auto.
    rewrite H_aux; clear H_aux.
    apply Zplus_lt_compat_r.
    apply Zgt_lt.
    apply Zgt_pos_0.

    apply Zle_0_pos.
Qed.

Lemma Qmult_le_compat_l:
  forall x y z : Q,
  x <= y ->
  0 <= z ->
  z * x <= z * y.
Proof.
  intros x y z H_x_le_y H_z_pos.
  rewrite Qmult_comm.
  assert (H_aux: z * y == y * z).
    rewrite Qmult_comm.
    reflexivity.
  rewrite H_aux; clear H_aux.
  apply Qmult_le_compat_r; auto.
Qed.

Lemma Qmult_lt_compat_l:
  forall x y z : Q,
  x < y ->
  0 < z ->
  z * x < z * y.
Proof.
  intros x y z H_x_lt_y H_z_pos.
  rewrite Qmult_comm.
  assert (H_aux: z * y == y * z).
    rewrite Qmult_comm.
    reflexivity.
  rewrite H_aux; clear H_aux.
  apply Qmult_lt_compat_r; auto.
Qed.