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

2. j :

3. j | i
4. q :

5. Div(i;j;q)

i-q

j = 0

By:	Unfold `div_nrel` 5 THEN Analyze 5 THEN Analyze 3

Generated subgoal:

1 3. c :
4. i = jc
5. q :
6. jqi
7. i<j(q+1)
i-qj = 0
3 steps

About:

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