How to prove a very basic algorithm by induction

I just studied proofs by induction on a math book here and everything is neat and funny: the general strategy is to assume the LHS to be true, and use it to prove the RHS (for the inductive step). Now I'm trying to prove the correctness of this algorithm for incrementing numbers, i.e. $y \rightarrow (y+1)$, but I have problems to bridge the gap between the two approaches.

Increment(y)
if y = 0 then return(1) else
if (y mod 2) = 1 then
return(2 * Increment(⌊y/2⌋))
else return(y + 1)

The beginning is easy:

1. Let $P(n)$ be $Inc(y)$

2. Base case: $P(0)$ is true because $Inc(y)$ returns 1

According to the algo book, if the number is even we're good since $y+1$ is explicitly returned.

Question 1: is this enough to build a complete proof? Or should I better lay out something like:

For the inductive step I assumed $P(n)$ to prove $P(n+1)$, i.e. $Inc(y) \rightarrow Inc(y+1)$; then: $$Inc(y) = y + 1 \rightarrow Inc(y+1) = y+2$$

and then say that adding 1 to both sides of the equation on the LHS gives the equation on the RHS therefore if the first one is true by assumption the second one has to be true as well? Is this completely trivial/redundant?

$$Inc(y) \rightarrow 2 \times Inc(\frac{y}{2})$$

and find a correlation between the two sides, thus using the assumed LHS to prove the RHS. On the other hand, the algo book sketches the proof as

We assume that the general case holds for all $y \leq n−1$

$$>2 · Increment(⌊(2m + 1)/2⌋) = 2 · Increment(⌊m + 1/2⌋) \\ >= 2 · Increment(m) \\ >= 2 (m+1) \\ >= 2m + 2 = y + 1 >$$

which I don't quite understand (what's up with the floor thing?) and I can't relate to my proof-template. For the matter, the algorithm is taken from the Algorithm Design Manual, page 16, freely available here.

TL;DR: I see that the algo works but I can't write a complete proof for it.

Your induction hypothesis is that $\,I(n) = n+1.\,$ The base case is true by the first line of the function. Assume it is true for all integers $< n.\,$ If $\,n = 2k\,$ then it is true by the last line of the function. Else $\, n = 2k+1\,$ so $\,n+1 = 2(k+1),\ k = \lfloor n/2\rfloor.\,$ But, by induction, $\,I(k) = k + 1,\,$ so the middle line returns $\, 2\, I(k) = 2(k+1) = n+1,\,$ which is correct. So the algorithm is correct both when $\,n\,$ is even or odd, which exhausts all possible cases for $\,n,\,$ completing the induction
for base case when $y=0$, it return $1$, for increment $y+1=0+1=1$ so it proved for base case, now for induction case for all $y\leq n-1$ it assumed to true,for general case we have to prove for $y+1$, if $y$ is even then it returns $y+1$, if $y+1$ is odd i.e. if $y=2m+1\leq2⋅Increment(⌊(m+1)/2⌋)\leq2\cdot Increment(⌊m+1/2⌋)\leq 2\cdot Increment(m)\leq2(m+1)\leq2m+2=(2m+1)+1$, given that $y=2m+1=y+1,$so it proved for increment $y+1$.