@@ -20,7 +20,7 @@ namespace Integer
20 divides val d
20 divides val d
21 = let dividend = if d < 0 then -(val `div` abs d)
21 = let dividend = if d < 0 then -(val `div` abs d)
22 else val `div` d
22 else val `div` d
23− remainder = val `mod` d in
23+ remainder = abs (val - dividend * d) in
24 believe_me (DivBy {d} {div = dividend} {rem = remainder}
24 believe_me (DivBy {d} {div = dividend} {rem = remainder}
25 (believe_me (Refl {x = True})))
25 (believe_me (Refl {x = True})))
@@ -56,7 +56,7 @@ namespace Int
56 divides val d
56 divides val d
57 = let dividend = if d < 0 then -(val `div` abs d)
57 = let dividend = if d < 0 then -(val `div` abs d)
58 else val `div` d
58 else val `div` d
59− remainder = val `mod` d in
59+ remainder = abs (val - dividend * d) in
60 believe_me (DivBy {d} {div = dividend} {rem = remainder}
60 believe_me (DivBy {d} {div = dividend} {rem = remainder}
61 (believe_me (Refl {x = True})))
61 (believe_me (Refl {x = True})))