(3steps total) PrintForm Definitions hol arithmetic 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsub wd
  and
  (all(m:hnum. equal(sub(0,m),0))
  ,all
  ,(m:hnum. all(n:hnum. equal(sub(suc(m),n),cond(lt(m,n),0,suc(sub(m,n)))))))
By: HN THEN Unab [`nnsub`] THEN Simp

Generated subgoals:

1 1. m : 
  if 0<m then 0 else 0-m fi  = 0  
1 step
2 1. m : 
2. n : 
  if m+1<n then 0 else m+1-n fi 
  =
  if m<n then 0 else if m<n then 0 else m-n fi +1 fi 
   
1 step

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

(3steps total) PrintForm Definitions hol arithmetic 2 Sections HOLlib Doc