Some definitions of interest.
le	Def  AB == B<A
	Thm*  i,j:. (ij)  Prop
ndiff	Def  a -- b == imax(a-b;0)
	Thm*  a,b:. (a -- b)
	Thm*  a,b:. (a -- b)
le_int	Def  ij == j<i
	Thm*  i,j:. (ij)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html