proposition: Lemma nthTailProp3 : forall (n : nat) (l : list rZ), length l <= n -> nthTail n l = nthTail (S n) l.
proof: Proof. intros n l H; rewrite (nthTailProp2 n l H); apply sym_eq; apply nthTailProp2; auto with arith stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet) Coq(Arith)