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

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.  }


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

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.

$$$$
`