Coq - Error when eliminating OR

Question

I don't know why, but in Coq, when trying to prove a program specification I get an error when trying to eliminate an OR hypothesis:

Error: Cannot find the elimination combinator or_rec, the elimination of the
inductive definition Logic.or on sort Set is probably not allowed.

This is the theorem I want to prove:

Definition nat_div_mod : forall a b:nat, not(b=0) -> {qr:nat*nat | P a b qr}.

This is the goal and context when the error happens:

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}

Before this theorem, I have this definition and these imports:

Definition P (a b:nat) (qr:nat*nat) : Prop := ... (* specification of div/mod *)
Require Import Omega.
Require Import Mult. 

I get the previous error when I try to use this tactic:

elim H0.

I don't really know what may be causing it.

Answer 1

You can't do case analysis on H0 because {qr : nat * nat | P (S a) b qr} is a Set or Type. Only or_ind is defined for or, so it would need to be a Prop instead. If you use sum you'll have sum_ind, sum_rec, and sum_rect.

(snd x < b - 1) + (snd x >= b - 1)

Prop is designed that way so that it's consistent with certain axioms.