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))

)