The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Marcus Ramos 
>>>>> <marcus.ramos AT univasf.edu.br>
>>>>>  writes:

> Thanks a lot!

Not sure if this is still of interest, but here's another way of getting to
skip_last without omega:

  Lemma big_enough : forall {X} n l,
    S n <= length l -> exists (x : X) xs, l = x :: xs.
  Proof.
    intros X n l.
    induction l; intros.
      inversion H.
    eauto.
  Qed.

  Lemma skip_last: forall (i: nat) (A: Type) (d: A) (l: list A),
    i < length l -> last (skipn i l) d = last l d.
  Proof.
    intros i A d l.
    generalize dependent i.
    induction l; intros.
      inversion H.
    destruct i; auto.
    simpl in *.
    apply Le.le_S_n in H.
    rewrite IHl.
      apply big_enough in H.
      destruct H. destruct H.
      rewrite H. reflexivity.
    apply H.
  Qed.

John