在引理的结论中搜索模式

当你知道它的结论应该是什么时，搜索一个引理：

Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m

你还可以搜索部分结论（结论和一个或几个最后的假设）。

Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

警告：如果你混淆了假设的顺序，你将找不到任何东西：

Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).