如何一步将一个定理分解为所有三个析取项？

Question

我已经证明了以下引理：

Lemma ord_semiconnex_bool : forall (alpha beta : ord),
  ord_ltb alpha beta = true \/ ord_ltb beta alpha = true \/ ord_eqb alpha beta = true.

我想为我正在证明的另一个定理对其进行案例分析，并尝试将其应用于对象：

gamma1 alpha1 : ord

但是如果我说：

destruct (ord_semiconnex_bool gamma1 alpha1).

这给了我两个分支而不是三个。在第一个分支中我得到：

H0 : ord_ltb gamma1 alpha1 = true

在第二个分支中我得到：

H0 : ord_ltb alpha1 gamma1 = true \/ ord_eqb gamma1 alpha1 = true

所以当我在第二个分支时，我一直在调用 "destruct H0"，为我提供我想要的两个进一步的子分支。但这很不雅致，结果我的证明看起来很难看。

有什么方法可以同时将我的定理分解为 3 个析取项？

Answer 1

destruct (...) as [ H1 | [ H2 | H3 ] ]