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

2. j :

3. c :

4. i = j

c
5. q :

6. j

i
7. i<j

(q+1)

i-q

j = 0

By:	(OnMClauses [0;6;7] (HypSubst 4)) THEN (Thin 4)

Generated subgoal:

1 4. q :
5. jqjc
6. jc<j(q+1)
jc-qj = 0
2 steps

About:

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