proposition: Lemma drop_tl_S: forall n (xs:Stream A), drop (S n) xs = tl (drop n xs).
proof: Proof. intros n; induction n; intros [x xs]; trivial. transitivity (tl (drop n xs)); trivial. rewrite drop_S_tl; trivial. Qed.
imports: List Streams Omega