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.