Nuprl - Proof: quot rem exists n sfa 1

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

1. b :

, r:

b. a = q

b+r

By:	CompNatInd Concl

Generated subgoal:

1 2. a :
3. a1:. a1<a (q:, r:b. a1 = qb+r)
q:, r:b. a = qb+r
6 steps

About:

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