Scanning through the theorems listed in the bottom part of the pcoq window, we discover that the theorem le_lt_trans is what we need. We are going to use this theorem by typing Apply le_lt_trans with m := y. in the top part of the pcoq window, then clicking on Do it. The result will be as in the following figure.