Nuprl - Proof: quot rem exists n sfa 1 1 2 1

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

1. b :

2. a :

a1:

. a1<a

(

, r:

b. a1 = q

b+r)
4.

a<b
5.

, r:

b. a-b = q

b+r

, r:

b. a = q

b+r

By:	ExistHD Hyp:-1

Generated subgoal:

1 5. q :
6. r : b
7. a-b = qb+r
q:, r:b. a = qb+r
2 steps

About:

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