1 files changed, 0 insertions, 15 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 53e8e86a..5530f8a7 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -610,18 +610,3 @@ type TickType;
 var $Tick: TickType;
 
 // ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// the connection between mod and div
-axiom (forall x:int, y:int :: {x mod y} {x div y}  x mod y == x - x div y * y);
-
-// remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x mod y}  0 < y  ==>  0 <= x mod y  &&  x mod y < y);
-axiom (forall x:int, y:int :: {x mod y}  y < 0  ==>  0 <= x mod y  &&  x mod y < -y);
-
-// the following axiom has some unfortunate matching, but it does state a property about mod that
-// is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b  ==>  a + d <= b);
-
-// ---------------------------------------------------------------