Nuprl - Proof: quot rem exists n sfa 1 1

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

1. b :

2. a :

a1:

. a1<a

(

, r:

b. a1 = q

b+r)

, r:

b. a = q

b+r

By:	Decide: a<b

Generated subgoals:

1 4. a<b
q:, r:b. a = qb+r
1 step

2 4. a<b
q:, r:b. a = qb+r
4 steps

About:

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

1	4. a<b q:, r:b. a = qb+r	1 step
2	4. a<b q:, r:b. a = qb+r	4 steps