a,b:, n:. ((a+bn) rem n) = (a rem n)

By:	Auto THEN Inst: Thm* i,j:. ij   Using:[b | n] THEN ElaborateDivision Auto 0

1

1. a :  2. b :  3. n :  4. bn   5. a+bn = ((a+bn)  n)n+((a+bn) rem n) 6. a = (a  n)n+(a rem n) 7. ((a+bn) rem n)  n 8. (a rem n)  n   ((a+bn) rem n) = (a rem n)

1 step

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