The Coq mailing list

[Krimo Nimour <nimour AT montrouge.tt.slb.com>]

Dear Coq team,

I want to prove the following subgoal:

1 subgoal

  n : nat
  i : nat
  HR : {m:nat | (i=(plus m m)\/i=(S (plus m m)))}
  j : nat
  I : i=(plus j j)\/i=(S (plus j j))
  ============================
   {m:nat | ((S i)=(plus m m)\/(S i)=(S (plus m m)))}

Trying "Elim I" produces: 

div2 < Elim I.
Error during interpretation of command:
Elim I.
Error: or_rec not declared

How can I decompose the hypothesis "I"?

Cordialement,
krimo.