proposition: Lemma drop_plus_tl:forall xs m n, drop m (drop n xs)=drop (m+n) xs.
proof: Proof. intros xs m n; generalize xs; clear xs. induction n; [ simpl; rewrite Plus.plus_0_r | replace (m+S n)%nat with ((m+n)+1)%nat; replace (S n) with (n+1)%nat; try abstract omega; intros xs; repeat rewrite <- drop_n_tl; rewrite <- (IHn (tl xs)) ]; trivial. Defined.
imports: List Streams Omega