IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quot rem exists111 1. a : 2. b : 3. 0a 4. q:, r:b. a = qb+r q:, r:b. a = qb+r
By:
Analyze 4 THEN Witness q
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html