(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:
1
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)
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc