At:
div rem properties2
1.
a:
2.
n:
3.
a = (a n)n+(a rem n)
4.
|a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)
a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)
By:
Auto
THEN
ThinTrivial
Generated subgoals:
n)
n+(a rem n)
a < 0) & ((a rem n) > 0 
a = (a