IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quot rem exists n sfa111 1. b : 2. a : 3. a1:. a1<a (q:, r:b. a1 = qb+r)
4. a<b q:, r:b. a = qb+r
By:
Witness: 0 | a
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a1:
(
q:
b+r)
