(a b) = -((-a) b) By: Inst
Thm*a:, n:. a = (a n)n+(a rem n)
[-a;b]
THEN
Inst
Thm*a:, n:. 0(a rem n) & (a rem n) < n
[-a;b]
THEN
Inst
Thm*a:, n:. a = (a n)n+(a rem n)
[a;b]
THEN
Inst
Thm*a:{...0}, n:. 0(a rem n) & (a rem n) > -n
[a;b] Generated subgoal: