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 !
un+p+2=un+1up+1+unup

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