证明Ssreflect中的简单不等式

Question

我在Coq中使用MathComp库进行反射时遇到了一些非常简单的证明.

假设我想证明这个引理:

From mathcomp Require Import ssreflect ssrbool ssrnat.

Lemma example m n: n.+1 < m -> n < m.
Proof.
      have predn_ltn_k k: (0 < k.-1) -> (0 < k).
          by case: k.
      rewrite -subn_gt0 subnS => submn_pred_gt0.
      by rewrite -subn_gt0; apply predn_ltn_k.
Qed.

对于这样一个简单的任务,这种方法对我来说似乎有些"非正统".有更好/更简单的方法吗？

Answer 1

是的,还有更好的方法.你的引理是一个特例ltnW : forall m n, m < n -> m <= n:

Lemma example n m : n.+1 < m -> n < m.
Proof. exact: ltnW. Qed.

这是有效的,因为n < m实际上是语法糖n.+1 <= m.