Nuprl - Proof: chrem exists 1 2 1 2

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

1. r :

2. s :

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

5. b :

6. p :

7. p = 1 mod r
8. p = 0 mod s
9. q :

10. q = 1 mod s
11. q = 0 mod r

p+b

q) = b mod s

By:	(RewriteWith [8;10] [] 0) THEN (ArithSimp 0)

Generated subgoal:

1 b = b mod s
1 step

About:

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