Nuprl - Proof: divides iff rem zero 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

2. j :

3. c :

4. q :

5. j

c
6. j

c<j

(q+1)

c-q

j = 0

By:	(FwdThru Thm* a,b:, n:. nanb ab [5]) THEN (FwdThru Thm* a,b:, n:. na<nb a<b [6]) THEN (OnHyps [6;5] Thin)

Generated subgoal:

1 5. qc
6. c<q+1
jc-qj = 0
1 step

About:

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