Nuprl - Proof: sub left suc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sub left suc

m,n:

. nnsub(m;n)+1 = if m

n then 0+1 else nnsub(m+1;n) fi

By:	RewriteOfThm Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. equal Thm* (m:hnum. (n:hnum. (suc(sub(m,n)) Thm* (m:hnum. (n:hnum. ,cond(le(m,n),suc(0),sub(suc(m),n))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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