Def   == {i:| 0<i }

is mentioned by

Thm*  x:, y,z:. x = yz  (x  z) = y	[div_inverts_nat_mul2]
Thm*  x,y:, z:. x = yz  (x  z) = y	[div_inverts_nat_mul]
Thm*  x,y:. xy	[mul_nat_plus]
Thm*  k:, i:{2..k}, j:. ij = k  2  j < k & i<k	[factors_smaller2]
Thm*  i:{2...}, j:. j<ij	[factor_smaller2]
Thm*  i,j:. iij & jij	[factors_bound]
Thm*  x,y:, z:. x<y  x<yz	[lt_mul_rt_by_pos]
Thm*  k:, n:, x,y:. kx+n = ky  xy	[factor_bound]
Thm*  x,y:, z:. xy  xyz	[le_mul_rt_by_pos]
Thm*  a,b:, n:. nanb  ab	[nat_factor_cancel_rw]

In prior sections: int 1 int 2 num thy 1

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