proposition: Lemma drop_n_tl:forall xs n, drop n (tl xs) = drop (n + 1) xs.
proof: Proof. intros [x xs]; induction n. reflexivity. replace (S n + 1) with (S (S n)); [reflexivity |abstract omega ]. Defined.
imports: List Streams Omega