Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
Natural Numbers

Robert Milewski

University of Bialystok
MML Identifier:
NAT_2
The terminology and notation used in this paper have been
introduced in the following articles
[11]
[14]
[2]
[5]
[12]
[1]
[8]
[10]
[9]
[6]
[4]
[13]
[7]
[3]

Preliminaries

Division and Rest of Division
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Grzegorz Bancerek.
Sequences of ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Jozef Bialas.
Group and field definitions.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
Journal of Formalized Mathematics,
5, 1993.
 [8]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
Journal of Formalized Mathematics,
2, 1990.
 [9]
Konrad Raczkowski and Andrzej Nedzusiak.
Series.
Journal of Formalized Mathematics,
3, 1991.
 [10]
Piotr Rudnicki and Andrzej Trybulec.
Abian's fixed point theorem.
Journal of Formalized Mathematics,
9, 1997.
 [11]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [12]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
 [13]
Wojciech A. Trybulec.
Pigeon hole principle.
Journal of Formalized Mathematics,
2, 1990.
 [14]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received February 23, 1998
[
Download a postscript version,
MML identifier index,
Mizar home page]