Def AB == B<A

is mentioned by

Thm* m,n,x:. nnsub(m;n) = x  m = n+x    mn & x0	[sub_right_eq]
Thm* m,n,x:. m = nnsub(n;x)  m+x = n    m0 & nx	[sub_left_eq]
Thm* m,n,x:. xnnsub(m;n)  n+xm  x0	[sub_right_greater_eq]
Thm* m,n,x:. nnsub(n;x)m  nm+x	[sub_left_greater_eq]
Thm* m,n,x:. nnsub(m;n)x  mn+x	[sub_right_less_eq]
Thm* m,n,x:. mnnsub(n;x)  m+xn  m0	[sub_left_less_eq]
Thm* m,n,x:. mn  (x+1)m(x+1)n	[mult_less_eq_suc]
Thm* m,n:. m+n+1m	[not_suc_add_less_eq]
Thm* m,n:. nm  m+1n	[not_greater_eq]
Thm* m,n:. n<m  mn	[not_greater]
Thm* m,n:. m = n  m+1n  n+1m	[not_num_eq]
Thm* m,n:. mn  n+1m	[not_leq]
Thm* n:. n+10	[not_suc_less_eq_0]
Thm* m,n,x:. m+nm+x  nx	[add_mono_less_eq]
Thm* m,n:. m = n  mn & nm	[eq_less_eq]
Thm* m,n,x:. m<n & nx  m<x	[less_less_eq_trans]
Thm* m,n,x:. mn & n<x  m<x	[less_eq_less_trans]
Thm* n:. n0  n = 0	[less_eq_0]
Thm* m,n:. mn  n<m	[not_less_equal]
Thm* m,n:. mn  (x:. n = m+x  )	[less_eq_exists]
Thm* m,n:. mn  (x:. n = m+x  )	[less_equal_add]
Thm* m,n:. mn  nm	[less_eq_cases]

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

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