Nuprl - Proof: nat prime div each factor 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat prime div each factor 1 1

1. X :

2. prime(X)
3.

. 0<W

W<X

(

. X | t

X | t)
4. a :

5. b :

6. X | a

X | a

X | b

By:	{divide a and b by X, reducing case split to remainders being zero } SideProof

Generated subgoal:

1 7. x :
8. r : X
9. a = xX+r
10. y :
11. s : X
12. b = yX+s
r = 0 s = 0
12 steps

About:

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