proposition: Lemma Str_nth_tl_plus : forall (n m:nat) (s:Stream), Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
proof: Proof. simple induction n; simpl; intros; auto with datatypes. rewrite <- H. rewrite tl_nth_tl; trivial with datatypes. Qed.