At:
div floor mod properties1
1.
a:
2.
n:
3.
0a
a = (a n)n+(a rem n) & (a rem n) < n
By:
Inst
Thm*a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)
[a;n]
THEN
MoveToConcl -3
THEN
Unfold `absval` 0
THEN
RepeatFor 2 SplitOnConclITE
Generated subgoals:
a
a = (a 
n)
n+(a rem n) & (a rem n) < n
a:
. a = (a 
a < 0) & ((a rem n) > 0