(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: rem addition 1 1 1 1 1 1 1
1. i:
2. j:
3. n:
4. 0(i rem n)
5. (i rem n) < n
6. 0(j rem n)
7. (j rem n) < n

0(i rem n)+(j rem n)
By: FwdThru Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 [4;6]
Generated subgoals:

None

About:
natural_numberaddremainderless_than

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc