Nuprl - Proof: hfact wd 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hfact wd 1

1. n :

fact(n+1) = (n+1)

fact(n)

By:	Assert (n+1>0) THEN Simp THEN Try (Complete Auto)

Generated subgoal:

1 2. n+1>0
(n+1)fact(n+1-1) = (n+1)fact(n)
1 step

About:

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