Def pre(n) == if n=0 then 0 else n-1 fi 

is mentioned by

Thm* n:. 0<n  (m:. pre(m)pre(n)  mn)	[inv_pre_less_eq]
Thm* m:. 0<m  (n:. pre(m)<pre(n)  m<n)	[inv_pre_less]
Thm* m,n:. 0<m & 0<n  (pre(m) = pre(n)  m = n)	[inv_pre_eq]
Thm* m,n:. 0<n  (m = pre(n)  m+1 = n  )	[pre_suc_eq]
Thm* m,n:. pre(nnsub(m;n)) = nnsub(pre(m);n)	[pre_sub]

In prior sections: hol prim rec

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