Nuprl - Proof: divides iff rem zero 1 1 1 1 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides iff rem zero 1 1 1 1 1 1 1 1 1

2. j :

3. c :

4. q :

5. q

c
6. c<q+1

c-q

j = 0

By:	(Using [`n',(jq)] (BackThru Thm* a,b,n:. a = b a+n = b+n)) THEN (Assert (jc = jq))

Generated subgoals:

None

About:

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