L. Fr_fib_sum2-i-j-k, fib i + fib j + fib k) = (i-j+1)/2 + ((j-k-1)./2) * (i-j+2)./2 + (k./2.-1)*( (i-j+1, pp.2-2

L. Fr_fib_sum4-i-j, 5 <= j -> j.+2 <= i -> FR(fib i + fib j + 2) = (i-j+1), pp.2-2

. Lemma-fib_times2-i, +2) * 2 = fib i.+3 + fib i. Lemma fib_times3 i: (fib i.+2) * 3 = fib i.+4 + fib i. Lemma fib_times4 i: (fib i.+2) * 4 = fib i, +4 + fib i.+2 + fib i

G. We-have, + x) and G j (x) = x/(1 ? x), assuming x non-zero. Obviously, G m is the inverse of G p . It happens that G j is the inverse of G i (note that G i (0) = 1; so that there is a discontinuity here)

J. Grimm and E. If, < x) then xI (Stern_bij_rec (Sba_m x) m) else xH else xH, Definition Stern_bij1 x := Stern_bij_rec x (snumden x).+1. Definition Stern_bij x := if

L. Stern_bij_rece, x:rat) n : 0 < x -> ((snumden x) < n)%N ->

. Lemma-stern_bij_gt0-x, Stern_bij x)%N. Lemma Stern_bij1_inj x y: 0 < x -> 0 < y ->

L. Ord3_trichot, I_3): (a == ord0) (+) (a == ord1_3) (+) (a == ord2_3

. Lemma, nseq (size l) ord0. Lemma wbase2_pad l k: wbase2 (l ++ nseq k ord0) = wbase2 l. Lemma wbase2_split l n: log2 n <= size l -> wbase2 l = n -> l = take

. Lemma-tcast_val, T: Type) m n (H: m = n) (l: m.-tuple T): tval (tcast H l) = tval l

I. Grimm, Lemma add_sternD a b c d n: sternD (a + c) (b + d) n = add_seq (sternD a b n)

. Stern, if b is at odd position then b is greater than a and c (note that b = a + c) If by " greater than " one means ?, then the result is obvious; otherwise u and v have to be non-zero. As a and c are consecutive on the previous row, one of the terms is at odd position: it follows by induction

. Lemma-sternd_sumc-u-v-n, Lemma sternD_sum_quo a b a' b' n : ((sternD_sum a b n) %:Q / (sternD_sum a, %N%:Q))%R

L. Sternd_positive-'n-k, 0 < k < 2^n -> 1 < nth 0 (stern11 n) k. Lemma sternD_middle' n : nth 0 (stern11 n.+1) (2^n) = 2. Lemma sternD_middle_contra' n k : nth 0

. Lemma-sternd_bezout-n-i, f := fun n i => nth 0 (stern11 n) i): i < 2 ^n -> (f n i) * (f n.+1 i, +1) = 1 + (f n i.+1) * (f n.+1 i)

S. So, )(i ) = S q+n (1, 1)(i ) = s(2 q+n + i )

J. L. Brown and J. , A new characterization of the Fibonacci numbers, Fibonacci Quaterly, vol.3, issue.1, 1965.

G. Cantor, Contributions to the Founding of the Theory of Transfinite Numbers, Trans. P. Jourdain, 1897.

L. Carlitz, A note on Fibonacci numbers, Fibonacci Quaterly, vol.2, issue.1, 1964.

E. Dijkstra and . Ewd578, More about the function " fusc " (a sequel to EWD570) http://www.cs.utexas, EWD578.PDF Selected Writings on Computing: A Personal Perspective, pp.0-387, 1976.

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, 2009.

M. Niqui, Exact arithmetic on the Stern???Brocot tree, Journal of Discrete Algorithms, vol.5, issue.2, 2007.
DOI : 10.1016/j.jda.2005.03.007

M. Niqui and Y. Bertot, QArith: Coq Formalisation of Lazy Rational Arithmetic, Types for Proofs and Programs, pp.309-323, 2004.
DOI : 10.1007/978-3-540-24849-1_20
URL : https://hal.archives-ouvertes.fr/inria-00077041

.. Maximal, 29 2.2.3 A characterization of the Fibonacci numbers, p.33