The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

Given a definition and lemma like:

Definition cyclic_successor (m setsize: nat) : nat :=

  if beq_nat m setsize then 1 else S m.

Lemma cyclic_successor_induction1 : forall m setsize: nat,

  1 <= m < setsize -> cyclic_successor m setsize = S m.

Clearly "beq_nat m setsize" always fails where "m < setsize". So, the proof should be trivial. But, when I attempt to use induction it creates new goals with larger successors because the definition is not inductive with a decreasing term. Which rewrite tactics that can be used here to equate the two conditions?

-George