Def AB == B<A

is mentioned by

Thm* a:, n:. 0(a mod n) & (a mod n)<n	[mod_bounds]
Thm* a:, n:, k:. k(a  n)  kna	[div_lbound_1]
Thm* a:, n:. 0(a  n)	[div_bounds_1]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n)<-n	[rem_bounds_4]
Thm* a:, n:. 0(a rem n) & (a rem n)<n	[rem_bounds_1]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1q2k-r2  q1q2	[division_mono2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2  q1q2	[division_mono1_sfa]
Thm* a,b:. (a -- b) = 0  ab	[ndiff_zero]
Thm* a,b,c:. aimin(b;c)  ab & ac	[imin_ub]
Thm* a,b,c:. imin(a;b)c  ac  bc	[imin_lb]
Thm* a,b,c:. aimax(b;c)  ab  ac	[imax_ub]
Thm* a,b,c:. imax(a;b)c  ac & bc	[imax_lb]
Thm* i:, n:. |i|n  -ni & in	[absval_ubound]
Thm* a,b:. 0ab	[mul_bounds_1a]
Thm* i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2	[multiply_functionality_wrt_le]
Thm* a,b:, n:. nanb  ab	[mul_cancel_in_le]
Thm* a,b:, n:. ab  nanb	[mul_preserves_le]
Thm* a,b,n:. ab  a+nb+n	[add_mono_wrt_le_rw]
Thm* i,j:. ij  i<j+1	[le_to_lt_rw]
Thm* i,j:. i<j  i+1j	[lt_to_le_rw]

In prior sections: int 1 bool 1 core

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