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 !
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.
Look at This file