@MISC{FIB_NUM.MIZ,
  AUTHOR = {Solovay, Robert M.},
  TITLE = {Fibonacci Numbers},
  ACKNOWLEDGEMENT = {My thanks to Freek Wiedijk for helping me learn
Mizar and to Piotr Rudnicki for instructive comments on an earlier version
of this article. This article was finished while I was visiting Bialystok
and Adam Naumowicz and Josef Urban helped me through some difficult
moments.},
  SECTION1 = {Fibonacci Commutes with gcd},
  SECTION2 = {Fibonacci Numbers and the Golden Mean},
  DAY = {19},
  MONTH = {April},
  YEAR = {2002},
  ADDRESS1 = {P. O. Box 5949
Eugene OR 97405
U. S. A.},
  SUMMARY = {We show that Fibonacci commutes with g.c.d.; we then 
derive the formula connecting the Fibonacci sequence with the roots of
the polynomial $x^2 - x - 1.$}}

