As a result of applying lt_le_trans to our goal, we now have two goals to prove, but only the first one is displayed in the middle part of the pcoq window. The first goal is easy to prove, as it is among the assumptions. To express this in one gesture, you can click on H in the middle part of the pcoq window with the right button of the mouse (this a proof-by-pointing action). This generates a command that you can execute by clicking on Do it. The other goal then appears. Here the statement to prove is equivalent to the hypothesis H0. You can finish the proof with a proof-by-pointing action on H0, then clicking on Do it.
It is now time to require that Coq record this proof in its theorem database. Type Qed. and click on Do it. You can now check that the definition is correctly entered by choosing the option Check last Definitions from the Coq menu. As a result, the pcoq view should take the following aspect:
This is the end of this very short demonstration of a working session with pcoq.