Nuprl - Pf rem_addition 1 1 1 1

1. i:
2. j:
3. n:

(((i rem n)+(j rem n)) rem n) = (((i rem n)+(j rem n)+((i n)+(j n))n) rem n)

By: RWH (LemmaC Thm* a,b:, n:. ((a+bn) rem n) = (a rem n)) 0

Generated subgoals:

1 0(i rem n)+(j rem n)

2 0(i n)+(j n)

3 (((i rem n)+(j rem n)) rem n) = (((i rem n)+(j rem n)) rem n)

About:

1	`0(i rem n)+(j rem n)`
2	`0(i n)+(j n)`
3	`(((i rem n)+(j rem n)) rem n) = (((i rem n)+(j rem n)) rem n)`