How to prove "$x \le y$" or "$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq?

Question

I have made the following code, and I'm in stuck.

---

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.

Answer 1

You can use the following tactic setoid_rewrite <- Z.gt_lt_iff at 2., and then use Ztrichotomy to conclude. To decompose a bit what happens, setoid_rewrite is a tactic that allows rewriting with other relations than equality, provided the contexts under which the rewriting happens is "nice enough". Concretely, here the relation we are rewriting with is logical equivalence <->, and we are rewriting under \/, which respects equivalence, so everything goes well. The <- part of the tactic is the equivalent of - in mathcomp, meaning we want to rewrite from right to left rather than left to right, and the at 2 part selects the part of the term we want to rewrite (the second one matching the conclusion of Z.gt_lt_iff).