diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
index d98dcd0b..ff6b274f 100644
--- a/src/Collections/Sequences/Seq.dfy
+++ b/src/Collections/Sequences/Seq.dfy
@@ -14,7 +14,7 @@
  *******************************************************************************/
 
 include "../../Wrappers.dfy"
-include "../../Math.dfy"
+include "../../MathLib.dfy"
 include "MergeSort.dfy"
 include "../../Relations.dfy"
 
@@ -23,7 +23,7 @@ module {:options "-functionSyntax:4"} Seq {
   import opened Wrappers
   import opened MergeSort
   import opened Relations
-  import Math
+  import MathLib
 
   /**********************************************************
    *
@@ -427,7 +427,7 @@ module {:options "-functionSyntax:4"} Seq {
     ensures Max(xs) in xs
   {
     assert xs == [xs[0]] + xs[1..];
-    if |xs| == 1 then xs[0] else Math.Max(xs[0], Max(xs[1..]))
+    if |xs| == 1 then xs[0] else MathLib.Max(xs[0], Max(xs[1..]))
   }
 
   /* The maximum of the concatenation of two non-empty sequences is greater than or 
@@ -453,7 +453,7 @@ module {:options "-functionSyntax:4"} Seq {
     ensures Min(xs) in xs
   {
     assert xs == [xs[0]] + xs[1..];
-    if |xs| == 1 then xs[0] else Math.Min(xs[0], Min(xs[1..]))
+    if |xs| == 1 then xs[0] else MathLib.Min(xs[0], Min(xs[1..]))
   }
 
   /* The minimum of the concatenation of two non-empty sequences is 
diff --git a/src/JSON/Serializer.dfy b/src/JSON/Serializer.dfy
index 1f936deb..fda9c9c1 100644
--- a/src/JSON/Serializer.dfy
+++ b/src/JSON/Serializer.dfy
@@ -9,7 +9,7 @@
 
 include "../Collections/Sequences/Seq.dfy"
 include "../BoundedInts.dfy"
-include "../Math.dfy"
+include "../MathLib.dfy"
 
 include "Utils/Views.dfy"
 include "Utils/Vectors.dfy"
@@ -20,7 +20,7 @@ include "Spec.dfy"
 
 module {:options "-functionSyntax:4"} JSON.Serializer {
   import Seq
-  import Math
+  import MathLib
   import opened Wrappers
   import opened BoundedInts
   import opened Utils.Str
@@ -83,7 +83,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
 
   function Number(dec: Values.Decimal): Result<jnumber> {
     var minus: jminus := Sign(dec.n);
-    var num: jnum :- Int(Math.Abs(dec.n));
+    var num: jnum :- Int(MathLib.Abs(dec.n));
     var frac: Maybe<jfrac> := Empty();
     var exp: Maybe<jexp> :-
       if dec.e10 == 0 then
@@ -91,7 +91,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
       else
         var e: je := View.OfBytes(['e' as byte]);
         var sign: jsign := Sign(dec.e10);
-        var num: jnum :- Int(Math.Abs(dec.e10));
+        var num: jnum :- Int(MathLib.Abs(dec.e10));
         Success(NonEmpty(JExp(e, sign, num)));
     Success(JNumber(minus, num, Empty, exp))
   }
diff --git a/src/Math.dfy b/src/Math.dfy
index 17cf15f2..4e1b26ae 100644
--- a/src/Math.dfy
+++ b/src/Math.dfy
@@ -5,7 +5,7 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Math {
+module {:options "-functionSyntax:4"} MathLib {
   function Min(a: int, b: int): int
   {
     if a < b