References
- [1] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.
- [2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6. Concatenation of finite sequences 1310.1007/s10817-017-9440-6.13
- [3] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1
- [4] Artur Kornilowicz. How to define terms in Mizar effectively. Studies in Logic, Grammar and Rhetoric, 18:67–77, 2009.
- [5] Piotr Rudnicki and Andrzej Trybulec. On the integrity of a repository of formalized mathematics. In Andrea Asperti, Bruno Buchberger, and James H. Davenport, editors, Mathematical Knowledge Management, volume 2594 of Lecture Notes in Computer Science, pages 162–174. Springer, Berlin, Heidelberg, 2003. doi:10.1007/3-540-36469-2_13.10.1007/3-540-36469-2_13
- [6] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.
- [7] Rafał Ziobro. Fermat’s Little Theorem via divisibility of Newton’s binomial. Formalized Mathematics, 23(3):215–229, 2015. doi:10.1515/forma-2015-0018.10.1515/forma-2015-0018
- [8] Rafał Ziobro. On subnomials. Formalized Mathematics, 24(4):261–273, 2016. doi:10.1515/forma-2016-0022.