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