Search for a lemma when you know what its conclusion ought to be:
Coq < SearchPattern (S _ <= _). le_n_S: forall n m : nat, n <= m -> S n <= S m
You can also search on a partial conclusion (the conclusion and one or several last hypotheses).
Coq < Require Import Arith. Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _). Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Warning: if you mix up the order of the hypotheses, you won't find anything:
Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).