Is there a tactic in Coq to make a hypothesis from applying two hypotheses?

Question

Suppose in Coq we have the following hypotheses:

x, y, z: Z
H : x < y
H0 : y < z

and I would like to introduce also the hypothesis

H1 : x < z

which follows from H and H0 using Z.lt_trans. Is there a better way to do this than the following?

assert (H1 : x < z). 
{ apply Z.lt_trans with y.
  exact H. exact H0.  }

Answer 1

You may for instance write specialize (Z.lt_trans _ _ _ H H0) as H1.

Answer 2

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.

```