(9steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
sym
2
2
1.
a:
, n:
. (a rem n) = (a rem -n)
a:
, n:
. (a rem n) = (a rem -n)
By:
UnivCD
THEN
Decide (n
0)
Generated subgoals:
1
2.
a:
3.
n:
4.
n
0
(a rem n) = (a rem -n)
2
2.
a:
3.
n:
4.
n
0
(a rem n) = (a rem -n)
About:
(9steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
0
(a rem n) = (a rem -n)
n0 (a rem n) = (a rem -n)
a:, n:
. (a rem n) = (a rem -n) a:, n:. (a rem n) = (a rem -n)0)0 (a rem n) = (a rem -n)n0 (a rem n) = (a rem -n)
