Nuprl - Proof: quot rem exists 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: quot rem exists 1 2 1

1. a :

2. b :

a
4. q :

5. r :

b
6. -a = q

b+r

, r:

b. a = q

b+r

By:	Decide (r = 0)

Generated subgoals:

1 7. r = 0
q:, r:b. a = qb+r
1 step

2 7. r = 0
q:, r:b. a = qb+r
1 step

About:

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

1	7. r = 0 q:, r:b. a = qb+r	1 step
2	7. r = 0 q:, r:b. a = qb+r	1 step