At:
div rem unique a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n)
By:
Auto
THEN
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]
Generated subgoal:
1. a: 2. n: 3. q: 4. r: 5. a = qn+r 6. |r| < |n| 7. r < 0 a < 0 8. r > 0 a > 0 9. a = (a n)n+(a rem n) 10. |a rem n| < |n| 11. (a rem n) < 0 a < 0 12. (a rem n) > 0 a > 0 q = (a n) & r = (a rem n)