Def   == {i:| 0<i }

is mentioned by

Thm*  a:, b:, f:({a..b}), j:{a..b}. Thm*  2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f)	[eval_reduce_factorization_less]
Thm*  a:, b:, f:({a..b}). {a..b}(f)	[eval_factorization_nat_plus]

In prior sections: int 1 int 2 num thy 1 SimpleMulFacts IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html