The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi,

I guess the following two list lemmas are correct, however I am not able to finish their proofs by myself. In case you have any hints or comments, I would be glad to hear about them.

Require Import List.

Lemma skip_hd:

forall i: nat,

forall A: Type,

forall d: A,

forall l: list A,

hd d (skipn i l) = nth i l d.

Lemma skip_last:

forall i: nat,

forall A: Type,

forall d: A,

forall l: list A,

i < length l -> last (skipn i l) d = last l d.

Thanks in advance,

Marcus.