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

At: rem addition 1 1 1 1 1 1

1. i:
2. j:
3. n:
4. 0(i rem n) & (i rem n) < n
5. 0(j rem n) & (j rem n) < n

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

By:
Analyze 5
THEN
Analyze 4


Generated subgoal:

14. 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)


About:
natural_numberaddremainderless_thanand

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