Nuprl - Proof: nnsub nuprl 1

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

1. m :

2. n :

3. m

if n<

m then 0 else n-m fi = n-m

By:	BifCase THEN Simp THEN StrongAuto

Generated subgoal:

1 4. n<m
0n-m
1 step

About:

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