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