Def le == m:. n:. mn

is mentioned by

Thm* all(n:hnum. implies(lt(0,n),all(k:hnum. le(div(k,n),k))))	[hdiv_less_eq]
Thm* all(n:hnum. all(m:hnum. equal(le(suc(n),suc(m)),le(n,m))))	[hless_eq_mono]
Thm* all(n:hnum. le(0,n))	[hzero_less_eq]
Thm* all(n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m))))	[hless_equal_antisym]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. implies(le(m,n),le(mult(m,p),mult(n,p))))))	[hless_mono_mult]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),le(m,n))))	[hless_imp_less_or_eq]
Thm* all(m:hnum. le(m,m))	[hless_eq_refl]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. implies Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. (and(le(m,p),le(n,q)) Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. ,le(add(m,n),add(p,q)))))))	[hless_eq_less_eq_mono]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. implies(and(le(m,n),le(n,p)),le(m,p)))))	[hless_eq_trans]
Thm* all Thm* (m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n)))))	[hless_eq_mono_add_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. implies Thm* (m:hnum. (n:hnum. (p:hnum. (le(n,p) Thm* (m:hnum. (n:hnum. (p:hnum. ,equal Thm* (m:hnum. (n:hnum. (p:hnum. ,(equal(add(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,,equal(m,sub(p,n)))))))	[hadd_eq_sub]
Thm* all(m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m))))	[hsub_add]
Thm* all(m:hnum. all(n:hnum. equal(equal(sub(m,n),0),le(m,n))))	[hsub_eq_0]
Thm* all(m:hnum. all(n:hnum. equal(not(lt(m,n)),le(n,m))))	[hnot_less]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),le(n,m)))))	[hless_eq_antisym]
Thm* all(m:hnum. le(m,suc(m)))	[hless_eq_suc_refl]
Thm* all(m:hnum. all(n:hnum. le(m,add(m,n))))	[hless_eq_add]
Thm* all(m:hnum. all(n:hnum. or(lt(m,n),le(n,m))))	[hless_cases]
Thm* all(m:hnum. all(n:hnum. equal(lt(m,n),le(suc(m),n))))	[hless_eq]
Thm* all(m:hnum. all(n:hnum. implies(le(suc(m),n),lt(m,n))))	[hor_less]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),le(suc(m),n))))	[hless_or]
Thm* all(m:hnum. all(n:hnum. equal(le(m,n),or(lt(m,n),equal(m,n)))))	[hless_or_eq]

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