@@ -20,7 +20,7 @@ namespace Integer
2020 divides val d
2121 = let dividend = if d < 0 then -(val `div` abs d)
2222 else val `div` d
23− remainder = val `mod` d in
23+ remainder = abs (val - dividend * d) in
2424 believe_me (DivBy {d} {div = dividend} {rem = remainder}
2525 (believe_me (Refl {x = True})))
2626
@@ -56,7 +56,7 @@ namespace Int
5656 divides val d
5757 = let dividend = if d < 0 then -(val `div` abs d)
5858 else val `div` d
59− remainder = val `mod` d in
59+ remainder = abs (val - dividend * d) in
6060 believe_me (DivBy {d} {div = dividend} {rem = remainder}
6161 (believe_me (Refl {x = True})))
6262