(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:, n:{...-1}. 0(a rem n) & (a rem n) < -n
[a;b] Generated subgoal: