At: div 3 to 11111 1. a: {...0} 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: