In addition to Pierre's answer, here are two more options.

First, you can use by transitivity y instead of having to dig through the library to discover Z.lt_trans:

Require Import ZArith.
Open Scope Z.

Lemma rabbit (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  assert (H1 : x < z).
  { now transitivity y. }
  trivial.
Qed.

Second, you can use ssreflect have tactic like this:

Require Import ZArith.
Open Scope Z.
From Coq Require Import ssreflect.

Lemma chicken (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  have H1 : x < z by transitivity y.
  trivial.
Qed.

```

In addition to Pierre's answer, here are two more options.

First, you can use transitivity y instead of having to dig through the library to discover Z.lt_trans:

Require Import ZArith.
Open Scope Z.

Lemma rabbit (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  assert (H1 : x < z).
  { now transitivity y. }
  trivial.
Qed.

Second, you can use ssreflect have tactic like this:

Require Import ZArith.
Open Scope Z.
From Coq Require Import ssreflect.

Lemma chicken (x y z : Z) (H : x < y) (H0 : y < z) : True.
Proof.
  have H1 : x < z by transitivity y.
  trivial.
Qed.

```