FTA DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Sections needed for FTA

FTAThe Fundamental Theorem of Arithmetic - unique prime factorizability
IteratedBinopsIterated Binary Operations
SimpleMulFactsSome handy lemmas about integer multiplication.
num thy 1Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven.
unionNon canonical functions (isl, outl, outr) for union type.
int 2
LogicSupplementSome handy basic lemmas about propositions and about types.
quot 1Support lemmas for quotient type.
rel 1Common properties of binary relations.
bool 1
int 1
well fnd
coreSome basic concepts defined type-theoretically.

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
FTA DiscrMathExt Doc