(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
invariant
1
2
1
1
1.
a:
2.
n:
3.
b:
4.
0+1
b
5.
((a+(b-1)
n) rem n) = (a rem n)
a+b
n
n
By:
Using [`n',n] (FwdThru
Thm*
a,b:
, n:
. a
b
n
a
n
b [4])
Generated subgoal:
1
6.
n
(0+1)
n
b
a+b
n
n
About:
(12steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(0+1)
nb
a+bn
n
bn) rem n) = (a rem n) a+bnn
a,b:, n:. ab 
nanb
[4])(0+1)nb a+bnn
