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

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

1. b :

2. a :

a1:

. a1<a

(

, r:

b. a1 = q

b+r)
4.

a<b

, r:

b. a = q

b+r

By:	FwdThru: 3 on [ a-b<a ]

Generated subgoal:

1 5. q:, r:b. a-b = qb+r
q:, r:b. a = qb+r
3 steps

About:

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