Now we need to know which theorems are available to prove a statement base on the predicate lt. For this we use the option Search with filter from the Coq menu. This opens a dialog box that has approximately the following shape:
Type lt in the bottom entry, which is labeled search for:, and click on Ok. After a few moments, the bottom part of the pcoq window is updated to provide the results of this search, yielding a window that looks as in the following figure.
