如何在Coq中同时对多个假设应用Nat.lt_le_incl引理？

• 方案1：手动指定目标假设
  原生apply in战术支持通过逗号分隔多个假设名实现批量应用，你的场景可以直接执行以下命令：

  apply Nat.lt_le_incl in H0, H1.
  

  执行后H0会变为a >= x，H1会变为a >= y，无需重复写两次战术。

• 方案2：自动匹配所有符合条件的假设
  如果需要处理的假设数量较多，不想手动逐个罗列名称，可以用match goal语法批量匹配处理：

  repeat match goal with
  | [ H : _ > _ |- _ ] => apply Nat.lt_le_incl in H
  end.
  

  该战术会自动遍历当前上下文里所有形式为严格大于的假设，逐一应用Nat.lt_le_incl完成转换。

之前的apply in *报错是因为原生Coq的apply战术不支持*通配符，只有clear、subst等少数战术支持该语法，apply in后必须接明确的假设名或用逗号分隔的假设名列表。

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