(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
addition
1
1.
i:
2.
j:
3.
n:
(((i rem n)+(j rem n)) rem n) = ((i+j) rem n)
By:
RWNth 2 (IfIsC i (LemmaWithC [`n',n]
Thm*
a:
, n:
. a = (a
n)
n+(a rem n))) 0
Generated subgoal:
1
(((i rem n)+(j rem n)) rem n) = (((i
n)
n+(i rem n)+j) rem n)
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(((i rem n)+(j rem n)) rem n) = (((i 
n)
n+(i rem n)+j) rem n)
(((i rem n)+(j rem n)) rem n) = ((i+j) rem n)
a:
, n:
. a = (a n)n+(a rem n)))
0 (((i rem n)+(j rem n)) rem n) = (((i n)n+(i rem n)+j) rem n)
