Nuprl - Pf rem_addition 1 1 1

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

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

By: Assert ((((i rem n)+(j rem n)) rem n) = (((i rem n)+(j rem n)+((i n)+(j n))n) rem n))

Generated subgoal:

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

About: