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

2. j :

3. j | i

i-(i

j = 0

By:	Inst Thm* a:, n:. q:. Div(a;n;q) & (a n) = q [i;j]

Generated subgoal:

1 4. q:. Div(i;j;q) & (i j) = q
i-(i j)j = 0
5 steps

About:

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