Search code examples
coqssreflect

Proving simple inequality in Ssreflect

I'm having trouble with some pretty simple proofs in Coq, using the MathComp library for reflection.

Suppose I want to prove this Lemma:

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.

This approach seems a little "unorthodox" to me for such a simple task. Is there a better/simpler way to do this?

Solution

  • Yes, there is a better way. Your lemma is a special case of ltnW : forall m n, m < n -> m <= n:

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

    This works because n < m is actually syntactic sugar for n.+1 <= m.