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

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Lemma Lem2 (a : Z) (b : Z) : 
(a<=b)%Z \/ (b < a)%Z.
Proof.
assert (H : (a < b)%Z \/ (a = b)%Z \/ (a > b)%Z).
{ apply Ztrichotomy. }
destruct H.
- left. 

And I could not proceed.