The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Quoting Giancarlo Bassi 
<g.bassi AT iperbole.bologna.it>:

> I'd like to know whether there's some .v file to handle proofs
> of the Fibonacci's numbers properties , like these ones:
>
> \sum_{k=1}^{n} F_{k} F_{k-1} = F_{n}^2
> \sum_{k=1}^{n} F_{k} = F_{n+2} - 1
> F_{n}^2 + F_{n+1}^2 = F_{2n+1} F_{n}^2 - F_{n-2} F_{n+2} = (-1)^{n}
> (F_{n-1} F_{n+2})^{2} + (2 (F_{n} F_{n+1})^2 = (F_{n}^2+ F_{n+1}^2)^2
>
> Thx
>
>
> Je voudrais savoir s'il y a un .v fichier pour executer la démonstration
> des propriétés des nombres de Fibonacci ci-dessus.
>
> Merci,  GB


Hi,

There are some properties of Fibonacci numbers in the following directories:
Not exactly the equalities above, but I hope it could help.

Pierre





http://www.labri.fr/perso/casteran/CoqArt/progav/
http://www.labri.fr/perso/casteran/CoqArt/gen-rec/

Pierre Castéran