Def nnsub(m;n) == if m<n then 0 else m-n fi 

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* b,c:. cb  (a:. nnsub(a;nnsub(b;c)) = nnsub(a+c;b))	[sub_sub]
Thm* a,b:. ba  (c:. nnsub(a;b)<c  a<b+c)	[less_eq_sub_less]
Thm* c:. nnsub(c;c) = 0	[sub_equal_0]
Thm* c,b:. cb  (a:. nnsub(a+b;c) = a+nnsub(b;c))	[less_eq_add_sub]
Thm* a,c:. nnsub(a+c;c) = a	[add_sub]
Thm* n,m,i:. i<nnsub(n;m)  i+m<n	[less_sub_add_less]
Thm* m,n:. n<m  nnnsub(m;1)	[sub_less_or]
Thm* n,m:. m<n  0<nnsub(n;m)	[sub_less_0]
Thm* m,n:. nnsub(m;n) = m  m = 0    n = 0	[sub_eq_eq_0]
Thm* n,m:. nnsub(n;m)n	[sub_less_eq]
Thm* a,b,c:. nnsub(a;b+c) = nnsub(nnsub(a;b);c)	[sub_plus]
Thm* n,m:. nnsub(n+1;m+1) = nnsub(n;m)	[sub_mono_eq]
Thm* m,n,x:. xnnsub(m;n) = nnsub(xm;xn)	[left_sub_distrib]
Thm* m,n,x:. nnsub(m;n)x = nnsub(mx;nx)	[right_sub_distrib]
Thm* m,n,x:. nx  (m+n = x    m = nnsub(x;n))	[add_eq_sub]
Thm* m,n:. pre(nnsub(m;n)) = nnsub(pre(m);n)	[pre_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:. nnsub(0;m) = 0 & nnsub(m;0) = m	[sub_0]

In prior sections: hol arithmetic 1

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