The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

That's probably not what you're looking for, but I couldn't resist 
advertizing this:

https://hal.inria.fr/hal-01195587/document
https://www.irif.fr/~letouzey/hofstadter_g/

tl;dr: playing with the recursive function g(n)=if n=0 then 0 else 
n-g(g(n-1)) leads to
strange worlds filled with Fibonacci numbers and fractal trees.

Regards
Pierre L.

----- Mail original -----
> Cool thanks!
> 
> I'm looking for analytic continuations of the continuous series as well as
> an alternative to starting at zero, and lastly some theoretic derivations
> of it's convergence point, with the work shown.
> 
> On Fri, Oct 27, 2017 at 2:51 AM, Laurent Thery 
> <Laurent.Thery AT inria.fr>
> wrote:
> 
> >
> >
> > On 10/26/2017 09:44 PM, Kenneth Adam Miller wrote:
> > > Hello,
> > >
> > > Does anybody know of any theorems or number theoretic work done using
> > > fibonacci in Coq?
> > >
> > > Thanks in advance!
> >
> > I don't know which results you have in mind. The mathcomp has only some
> > basic properties of the fib function
> >
> > https://github.com/math-comp/math-comp/blob/master/mathcomp/attic/fib.v
> >
> > --
> > Laurent
> >
> > Ps: fib.v is not part of the standard  mathcomp library
> >
>