The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Hi Adam,

> I wonder how one can persuade Coq that the Fixpoint definition is
> well-formed if the decrease of the argument is not completely obvious.

Have you tried well founded induction ?
Just grep for it in Coq's standard library.
I am sure Coq'art has nice examples illustrating how all this works.

Cheers,
Sébastien.