1. m : 
2. a : 
3. a' : 
4. b : 
5. b' : 
6. m | a-a'
7. m | b-b'
  m | a+b-(a'+b')

By:	(FwdThru Thm* a,b1,b2:. a | b1  a | b2  a | b1+b2 [6;7]) THEN (OnMClauses [-1;0] ArithSimp)

None

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