df-bottom Show Code edit
## Definition of denominator
##
## The numerator or bottom of a rational number. This is the same as the tail of an
## ordered pair. This definition is just a way of explaining that the tail
## of the ordered pair is the denominator. The tail of the ordered pair is expected
## to be in the format of an integer. This is only used in the construction of the rationals. It is
## ambiguous since the number 1/2, could be represented as 1/2, 2/4, or 6/12 and the bottom value
## would be different in each case. Thus all the theorems in the construction of the rationals
## assume that we do not know the value of bottom, we only know the ratio between the top and bottom
## values.
##
defthm (df-bottom nat (bottom A) () () (z.= (bottom A) (z.tail A))
(z.tail A) z.eqid
(z.= (z.tail A) (z.tail A))
)
edit