Nuprl - Proof: chrem exists aux a 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: chrem exists aux a 1 1 1 1

1. r :

2. s :

3. CoPrime(r,s)
4. x :

5. y :

6. r

x+s

y = 1

((s

y) = 1 mod r) & ((s

y) = 0 mod s)

By:	RevHypSubst 6 0

Generated subgoal:

1 ((sy) = (rx+sy) mod r) & ((sy) = 0 mod s)
3 steps

About:

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