(9steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsuc def
  all(m:hnum. equal(suc(m),abs_num(suc_rep(rep_num(m)))))
By: HN THEN StrongAuto

Generated subgoal:

1 1. m : 
  m+1 = abs_num(suc_rep(rep_num(m)))  
8 steps

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

(9steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc