Доказательство простого неравенства в 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,

Answer 2

Я не много практиковал ssreflect, поэтому я не могу точно сказать, можно ли это отыграть, но в основном идея заключается в том, что n < n.+1 < m:

Require Import mathcomp.ssreflect.ssrnat.
Require Import mathcomp.ssreflect.ssrbool.
Require Import mathcomp.ssreflect.ssreflect.

Lemma example m n: n.+1 < m -> n < m.
Proof.
move => ltSnm; apply: ltn_trans; by [apply ltnSn | apply ltSnm].
Qed.