I make the following code, and I'm in stuck. Please help me.

From mathcomp Require Import all_ssreflect.

Require Import QArith.


Lemma Lem1 (x : Q) (y : Q) :
not (x <= y) <-> x > y.
Proof.
split. apply Qnot_le_lt. apply Qlt_not_le.
Qed.

Lemma Zlt_or_eq (n : Z) (m : Z) :
(n < m)%Z \/ (n = m)%Z <-> (n <= m)%Z.
Proof.
assert (H : (n = m)%Z = (inject_Z n == inject_Z m)).
{ unfold inject_Z. unfold Qeq. simpl.
  rewrite Z.mul_comm. rewrite Z.mul_1_l.
  rewrite Z.mul_comm. rewrite Z.mul_1_l. reflexivity. }
rewrite Zle_Qle. rewrite Zlt_Qlt. rewrite H.
rewrite Qle_lteq. reflexivity.
Qed.

Theorem Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.
rewrite Lem1. unfold Qle. unfold Qlt.
rewrite -Zlt_or_eq.

Edit : Sorry, my question is about $\mathbb{Q}$, however my previous theorem is related to $\mathbb{Z}$. I edit it.

When I go to the last line, I want to apply Ztrichotomy, $$\forall n, ~m : \mathbb{Z} ~:~ n < m ~\lor ~ n = m ~ \lor ~ n > m.$$

However, my last term is (Qnum y * QDen x < Qnum x * QDen y)%Z,

instead of (Qnum x * QDen y > Qnum y * QDen x)%Z.

I want to change the order direction in Z-scope.