如何将(S n' <=? m) = true应用于S n' <= m？Coq证明求助

你不需要自己定义新引理，Coq标准库已经提供了布尔比较<=?和命题式比较<=之间的关联引理：

• 直接使用Nat.leb_le引理，它的类型为forall n m : nat, (n <=? m) = true -> n <= m，完全匹配你的场景。假设你的假设名为H，可以执行：

  apply Nat.leb_le in H.
  

  或者直接对目标应用引理完成证明：

  apply Nat.leb_le.
  

• 如果记不清引理名称，可通过搜索命令定位相关标准库内容：

  Search ((_ <=? _) = true -> _ <= _).
  

  该命令会列出所有符合条件的引理，从中挑选适用的即可。

如果你之前尝试自定义leb_true失败，大概率是因为没有通过归纳法完成严谨证明，但既然标准库已有成熟实现，直接复用更高效。

内容的提问来源于stack exchange，提问作者VikramG