(10steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: chrem exists 1 2 1 1

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
  (ap+bq) = a mod r


By: (RewriteWith [7;11] [] 0) THEN (ArithSimp 0)


Generated subgoal:

1   a = a mod r
1 step

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

(10steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc