Def AB == B<A

is mentioned by

Thm* x,n,m:. xn & xm  (nnsub(n;x) = nnsub(m;x)  n = m)	[cancel_sub]
Thm* x,n,m:. nx & mx  (nnsub(x;n) = nnsub(x;m)  n = m)	[sub_cancel]
Thm* m,x:. mx  (n:. nnsub(x;m)n  xm+n)	[sub_less_eq_add]
Thm* n,m:. nm  n<m+1	[less_eq_imp_less_suc]
Thm* b,c:. cb  (a:. nnsub(a;nnsub(b;c)) = nnsub(a+c;b))	[sub_sub]
Thm* n,m:. n+1m  mn	[not_suc_less_eq]
Thm* a,b:. ba  (c:. nnsub(a;b)<c  a<b+c)	[less_eq_sub_less]
Thm* c,b:. cb  (a:. nnsub(a+b;c) = a+nnsub(b;c))	[less_eq_add_sub]
Thm* m,n:. n<m  nnnsub(m;1)	[sub_less_or]
Thm* n,m:. nnsub(n;m)n	[sub_less_eq]
Thm* n:. 0<n  (m:. pre(m)pre(n)  mn)	[inv_pre_less_eq]
Thm* n:. 0<n  (k:. ndiv(k;n)k)	[div_less_eq]
Thm* n,m:. n+1m+1  nm	[less_eq_mono]
Thm* n:. 0n	[zero_less_eq]
Thm* n,m:. nm & mn  n = m	[less_equal_antisym]
Thm* m,n,x:. mn  mxnx	[less_mono_mult]
Thm* m,n:. m<n  mn	[less_imp_less_or_eq]
Thm* m:. mm	[less_eq_refl]
Thm* m,n,x,q:. mx & nq  m+nx+q	[less_eq_less_eq_mono]
Thm* m,n,x:. mn & nx  mx	[less_eq_trans]
Thm* m,n,x:. m+xn+x  mn	[less_eq_mono_add_eq]
Thm* m,n,x:. nx  (m+n = x    m = nnsub(x;n))	[add_eq_sub]
Thm* m,n:. nm  nnsub(m;n)+n = m	[sub_add]
Thm* m,n:. nnsub(m;n) = 0  mn	[sub_eq_0]
Thm* m,n:. m<n  nm	[not_less]
Thm* m,n:. (m<n & nm)	[less_eq_antisym]
Thm* m:. mm+1	[less_eq_suc_refl]
Thm* m,n:. mm+n	[less_eq_add]
Thm* m,n:. m<n  nm	[less_cases]
Thm* m,n:. m<n  m+1n	[less_eq]
Thm* m,n:. m+1n  m<n	[or_less]
Thm* m,n:. m<n  m+1n	[less_or]

In prior sections: int 1 bool 1 hol arithmetic 1 int 2 core

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