Nuprl - Pf rem_invariant 1

1. a:
2. b:
3. n:

((a+bn) rem n) = (a rem n)

By: NInd 2

Generated subgoals:

1 2. n:
((a+0n) rem n) = (a rem n)

2 2. n:
3. b:
4. 0 < b
5. ((a+(b-1)n) rem n) = (a rem n)
((a+bn) rem n) = (a rem n)

About:

1	2. `n:` `((a+0n) rem n) = (a rem n)`
2	2. `n:` 3. `b:` 4. `0 < b` 5. `((a+(b-1)n) rem n) = (a rem n)` `((a+bn) rem n) = (a rem n)`