# 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+1}u_{p+1}+u_{n}u_{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

Going home

Pierre Castéran