Nuprl - Proof: multiply functionality wrt eqmod 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: multiply functionality wrt eqmod 1 1 1

1. m :

2. a :

3. a' :

4. b :

5. b' :

6. m | (a-a')

b
7. m | (b-b')

a'
8. m | (a-a')

b+(b-b')

m | a

b-a'

By:	OnMClauses [0;8] ArithSimp

Generated subgoals:

None

About:

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