Q:

Inductive proof on scala stream

Can someone help me with how to reason inductively that this scala code
lazy val y : Stream[Int] = 1 #:: (y map (_ + 1))

produces a list of natural numbers from 1 onwards?

A:

The value at position in 1 #:: whatever is 1, so we know y(0) = 1.
At a greater position we have y(n+1) = whatever(n). Here whatever is y map (_+1), so y(n+1) = (y map (_+1))(n). 
We want to prove forall n. y(n) = n + 1. 
We know this is true for n = 0, y(0) = 1
(y.map(_+1))(n) is simply y(n) + 1. This is what map does. So our formula above becomes y(n+1) = y(n) + 1. 
Then trivially, if we know y(n) = n+1, then y(n+1) = (n+1) + 1. Result true at next rank. We get our proof by induction. 

