df-fraction Show Code edit
## Definition of Fraction
##
## A fraction is just an ordered pair of integers. This definition signals to the
## typesetter that the number should be displayed as a fraction and not an ordered pair.
##
## Definition of Fraction
defthm (df-fraction nat (</> A B) () () (z.= (</> A B) (z.<,> A B))
(z.<,> A B) z.eqid
(z.= (z.<,> A B) (z.<,> A B))
)
edit