(9steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
bounds
z
2
2
1.
a:
, b:
. |a rem b| < |b|
2.
a:
3.
b:
4.
0
b
|a rem b| < |b|
By:
RWH (RevLemmaC
Thm*
a:
, b:
. (a rem -b) = (a rem b)) 0
THEN
RWN 2 (LemmaC
Thm*
i:
. |i| = |-i|) 0
Generated subgoal:
1
|a rem -b| < |-b|
About:
(9steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
|a rem -b| < |-b|
a:
, b:
. |a rem b| < |b|
0
b |a rem b| < |b|a:, b:. (a rem -b) = (a rem b))
0
i:. |i| = |-i|)
0 |a rem -b| < |-b|
