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

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.

My trial is as follows :

From mathcomp Require Import all_ssreflect.

Require Import QArith.

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

Lemma Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.
rewrite Lem1.

And I could not proceed.