At: div 4 to 11111 1. a: 2. b: {...-1} 3. 0(a rem -b) 4. (a rem -b) < -b 5. 0(a rem b) 6. (a rem b) < -b 7. a+b(a (-b)) = (a rem -b) 8. a+-b(a b) = (a rem b)
(a b) = -(a (-b)) By: RevHypSubst 7 3
THEN
RevHypSubst 7 4
THEN
RevHypSubst 8 5
THEN
RevHypSubst 8 6
THEN
OnHyps [8;7] Thin Generated subgoal: