IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quot rem exists n sfa11211 1. b : 2. a : 3. a1:. a1<a (q:, r:b. a1 = qb+r)
4. a<b 5. q : 6. r : b 7. a-b = qb+r q:, r:b. a = qb+r
By:
Witness: q+1 | r
Generated subgoal:
1
a = (q+1)b+r
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a1:
(
q:
b+r)
a<b
