The Coq mailing list

[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