You can now enter a theorem to prove. Let's take a silly one to start with:
Theorem le_gt_trans : (x,y,z:nat)(le x y) -> (gt z y) -> (lt x z).
Enter the mouse in the top part of the pcoq window, and type this text, then click on Do it. Here again, the text of the command is parsed, and it is redisplayed in a different way, closer to usual mathematical conventions. Also, the statement of the theorem we want to prove is repeated in the middle part of the pcoq window. The pcoq window should now look as in the following figure.