我不知道为什么，但是在 Coq 中，当试图证明程序规范时，在试图消除 OR 假设时会出错：
Error: Cannot find the elimination combinator or_rec, the elimination of the
inductive definition Logic.or on sort Set is probably not allowed.
这是我要证明的定理：
Definition nat_div_mod : forall a b:nat, not(b=0) -> {qr:nat*nat | P a b qr}.
这是发生错误时的目标和上下文：
a : nat
b : nat
H : b <> 0
IHa : {qr : nat * nat | P a b qr}
x : nat * nat
H2 : P a b x
H0 : snd x < b - 1 \/ snd x >= b - 1
______________________________________
{qr : nat * nat | P (S a) b qr}
在这个定理之前，我有这个定义和这些导入：
Definition P (a b:nat) (qr:nat*nat) : Prop := ... (* specification of div/mod *)
Require Import Omega.
Require Import Mult.
当我尝试使用这种策略时，我得到了之前的错误：
elim H0.
我真的不知道可能是什么原因造成的。