@misc{NEWTON02.MIZ,
  AUTHOR = {Ziobro, Rafa{\l}},
  TITLE = {Fermat's Little Theorem via Divisibility of {N}ewton's Binomial},
  ADDRESS1 = {Department of Carbohydrate Technology,
    University of Agriculture in Krakow},
  DAY = {30},
  MONTH = {June},
  YEAR = {2015},
  SECTION1 = {Divisibility of Newton's Binomial},
  SECTION2 = {Fermat's Little Theorem Revisited},
  ACKNOWLEDGEMENT = {Ad Maiorem Dei Gloriam},
  SUMMARY = {Solving equations in integers is an important
  part of number theory \cite{sierpinski1956}.
  In many cases it can be done by factorization of equation's
  elements, such as Newton's binomial.
  The article introduces several simple formulas, which
  may facilitate this process.
  Some of them are taken from relevant books \cite{sierpinski1950},
  \cite{gancarzewicz2000}.
  \par
  In the second section of the article,
  Fermat's Little Theorem is proved in a classical way,
  on the basis of divisibility of Newton's binomial.
  Although slightly redundant in its content (other proof of
  the theorem has earlier been included in \cite{EULER_2.ABS}),
  the article provides a good example, how the application of
  registrations could shorten the length of Mizar
  proofs \cite{caminati2013custom}, \cite{kornilowicz2013rewriting}.}}

@article{sierpinski1950,
title={Teoria liczb},
author={Sierpi{\'n}ski, Wac{\l}aw},
year={1950},
publisher={Instytut Matematyczny Polskiej Akademii Nauk},
NOTE = {in Polish}}

@misc{sierpinski1956,
title={O rozwi\c{a}zywaniu rowna\'{n} w liczbach ca{\l}kowitych},
author={Sierpi{\'n}ski, Wac{\l}aw},
year={1956},
publisher={Warszawa}}

@misc{gancarzewicz2000,
title={Arytmetyka},
author={Gancarzewicz, Jacek},
year={2000},
publisher={Wydawnictwo UJ, Krak{\'o}w}}

@article{caminati2013custom,
  title={Custom Automations in Mizar},
  author={Caminati, Marco Bright and Rosolini, Giuseppe},
  journal={Journal of automated reasoning},
  volume={50},
  number={2},
  pages={147--160},
  year={2013},
  publisher={Springer}}

@article{kornilowicz2013rewriting,
  title={On Rewriting Rules in Mizar},
  author={Korni{\l}owicz, Artur},
  journal={Journal of Automated Reasoning},
  volume={50},
  number={2},
  pages={203--210},
  year={2013},
  publisher={Springer}}
