(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
4
to
1
1
1
1.
a:
2.
n:
{...-1}
a-(a
n)
n = a-(a
(-n))
(-n)
By:
Rewrite (NthC 1 (LemmaC
Thm*
a:
, b:{...-1}. (a
b) = -(a
(-b)))) 0
Generated subgoal:
1
a-(-(a
(-n)))
n = a-(a
(-n))
(-n)
About:
(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
a-(-(a 
(-n)))
n = a-(a (-n))(-n)
a-(a n)n = a-(a (-n))(-n)
a:, b:{...-1}. (a b) = -(a (-b))))
0 a-(-(a (-n)))n = a-(a (-n))(-n)
