The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hello,

While reading Section 4.5.3 of the Reference Manual (Well-formed inductive 
definitions)
and while going through the standard library, I have try to define this:

  (* a superfluous definition of "ge" predicate *)
  Inductive ge (n:nat) : nat -> Prop :=
    | ge_n : ge n n
    | ge_S : forall m:nat, ge n m -> ge (S n) m.

Coq rejects that definition with a message:

  Error: Last occurrence of "ge" must have "n" as 1st argument in
  "forall m : nat, ge n m -> ge (S n) m".

That is somewhat surprising because the definition (despite being superfluous 
in practise) seems plausible to me.

If I may, I would like to ask:
- which side-condition of the W-Ind rule (?) the definition above breaks?
- why that kind of restriction must be enforced?