x = (x n)n+(x rem n)

(x rem n) < 0 x < 0

(x rem n) > 0 x > 0

y = (y n)n+(y rem n)

(y rem n) < 0 y < 0

(y rem n) > 0 y > 0

(x rem n)+(y rem n) = (((x rem n)+(y rem n)) n)n+(((x rem n)+(y rem n)) rem n)

(((x rem n)+(y rem n)) rem n) < 0 (x rem n)+(y rem n) < 0

(((x rem n)+(y rem n)) rem n) > 0 (x rem n)+(y rem n) > 0

x+y = 0

((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi

Inst Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n) [x+y;n;(x n)+(y n)+(((x rem n)+(y rem n)) n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))if n < 0 -1 else 1 fi ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)if n < 0 1 else -1 fi else 0 fi;(((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi]

1	x+y = ((x n)+(y n)+(((x rem n)+(y rem n)) n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))if n < 0 -1 else 1 fi ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)if n < 0 1 else -1 fi else 0 fi)n+(((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi	1 step
2	|(((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi| < |n|	1 step
3	17. (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi < 0 x+y < 0	2 steps
4	17. (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi > 0 x+y > 0	2 steps

About: