Coq/SSReflect：(x < y) + (x == y) + (y < x)？

Question

在vanilla Coq中，我会写道

Require Import Coq.Arith.Arith.
Goal nat -> nat -> False.
  intros n m.
  destruct (lt_eq_lt_dec n m) as [[?|?]|?].

获得三个目标，一个是n < m，一个是n = m，还有一个是m < n。在ssreflect中，我会从

From Coq.ssr Require Import ssreflect ssrbool.
From mathcomp.ssreflect Require Import eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.

在ssreflect中，将这种情况分为三种情况的标准/规范方法是什么?对于n < m、n == m和m < n？

Answer 1

您可以使用ltngtP

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.
  case: (ltngtP n m) => [n_lt_m|m_lt_n|n_eq_m].

根据ssreflect风格，该引理自动简化了目标中的比较函数，如n < m、n == m等。