The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Fixpoint list_of_nats n len: list nat :=

 match n with O => cons len nil | S m => cons (len - n) (list_of_nats m len) end.

Theorem list_of_nats_nth {k n} len default (p: k <= n): nth k (list_of_nats n len) default = len + k - n.

Admitted.

I can't prove it for long time already. Any hints are very appreciated.