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

At: rem addition 1 1 1 1 1

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

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

By:
Inst Thm* a:, n:. 0(a rem n) & (a rem n) < n [i;n]
THEN
Inst Thm* a:, n:. 0(a rem n) & (a rem n) < n [j;n]


Generated subgoal:

14. 0(i rem n) & (i rem n) < n
5. 0(j rem n) & (j rem n) < n
0(i rem n)+(j rem n)


About:
natural_numberaddremainder

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