proposition: Lemma nthTailProp1 : forall (n : nat) (l : list rZ), n < length l -> nthTail n l = myNth n l rZTrue :: nthTail (S n) l.
proof: Proof. simple induction n. intros l; case l; simpl in |- *; intros; auto with stalmarck; absurd (0 < 0); auto with arith stalmarck. intros n' HR l; case l; simpl in |- *; [ intros H; absurd (S n' < 0) | intros t l' H; rewrite (HR l') ]; auto with arith stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet) Coq(Arith)