(17steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
mag
bound
1
1
1
1
1.
a:
2.
n:
3.
0
n
|a rem n| < n
By:
RWH (UnfoldTopC `absval`) 0
THEN
BoolCasesOnCExp (0
(a rem n))
THEN
AbReduce 0
Generated subgoals:
1
4.
0
(a rem n)
(a rem n) < n
2
4.
(a rem n) < 0
-(a rem n) < n
About:
(17steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(a rem n)
(a rem n) < n -(a rem n) < n
n |a rem n| < n
(a rem n))
(a rem n) (a rem n) < n -(a rem n) < n
