Proving simple inequality in Ssreflect

1
votes

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?

2
coqssreflect
Please always include the list of imports when you're posting a code snippet. – gallais

2 Answers

5
votes

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.

1
votes

I haven't practiced ssreflect a lot so I can't really tell whether this can be golfed down but basically the idea is that 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.