Nuprl - Proof: quot rem exists 1 2 1 1

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

1. a :

2. b :

a
4. q :

5. r :

b
6. -a = q

b+r
7. r = 0

, r:

b. a = q

b+r

By:	InstConcl [-q;0]

Generated subgoals:

None

About:

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