Def  AB == B<A

is mentioned by

Thm*  x:{2...}. p:{2...}. px & prime(p) & p | x	[prime_or_smaller_prime_factor]
Thm*  x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc	[prime_or_smaller_prime_factor2]
Thm*  x:. prime(x)  2x	[natprimes_lb]
Thm*  x:. prime(x)  2x & (i:{2..x}. i | x)	[prime_nat]
Thm*  i,j:. 0<ij  iij & jij	[pos_mul_arg_boundsNat2]
Thm*  i,j:. iij & jij	[factors_bound]
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 bool 1 int 2 num thy 1 core

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