At: div 3 to 1111 1. a: {...0} 2. b: {...-1} 3. -a = ((-a) (-b))(-b)+((-a) rem -b) 4. 0((-a) rem -b) 5. ((-a) rem -b) < -b 6. a = (a b)b+(a rem b) 7. 0(a rem b) 8. (a rem b) > b
(a b) = ((-a) (-b)) By: Using [`n',(b((-a) (-b)))]
(FwdThru
Thm*a,b,n:. a = b a+n = b+n
[3])
THEN
Using [`n',((-b)(a b))]
(FwdThru
Thm*a,b,n:. a = b a+n = b+n
[6])
THEN
OnMHyps [-1;-2] ArithSimp
THEN
OnHyps [6;3] Thin Generated subgoal:
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))