Solution (source code)

= Solution

Fix $m\ge1$ and use two-base <mathematical induction> on $n$. At $n=0$, the proposed right side is $F_m$; at $n=1$, it is $F_{m-1}+F_m=F_{m+1}$. Suppose the identity holds at $n$ and $n+1$. The defining <recurrence relation> for the <Fibonacci numbers> gives
$$
F_{m+n+2}=F_{m+n+1}+F_{m+n}
=F_{m-1}(F_{n+1}+F_n)+F_m(F_{n+2}+F_{n+1})
=F_{m-1}F_{n+2}+F_mF_{n+3}.
$$
This is the assertion at $n+2$, completing the proof of the <Fibonacci addition formula>. The argument includes $m=1$, since $F_{m-1}=F_0$ is defined.