(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: rem 2 to 1 1 1

1. a: {...0}
2. n:

a-(a n)n = -(-a-((-a) n)n)

By: Rewrite (NthC 1 (LemmaC Thm* a:{...0}, b:. (a b) = -((-a) b))) 0

Generated subgoal:

1 a-(-((-a) n))n = -(-a-((-a) n)n)


About:
intnatural_numberminussubtractmultiplydivideequal

(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc