Reasoning on the Fibonacci sequence

The theorem nat_ind is not very useful for reasoning on the fibonacci function . Try for example to prove the following equality !

u_n+p+2=u_n+1u_p+1+u_nu_p

In order to prove some properties like above, it is useful to prove an ad-hoc induction principle.
Design this induction principle, prove it, and use it to prove the equality above.

Solution

Look at This file