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

Going home
Pierre Castéran