diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index c0e94d9639..f1f19f3fc0 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -19,8 +19,8 @@ def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint8_mod"]
 def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
-def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
+@[deprecated UInt8.mod (since := "2024-09-23")]
+def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint8_land"]
 def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint8_lor"]
@@ -79,8 +79,8 @@ def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint16_mod"]
 def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
-def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
+@[deprecated UInt16.mod (since := "2024-09-23")]
+def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint16_land"]
 def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint16_lor"]
@@ -141,8 +141,8 @@ def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint32_mod"]
 def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
-def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
+@[deprecated UInt32.mod (since := "2024-09-23")]
+def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint32_land"]
 def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint32_lor"]
@@ -184,8 +184,8 @@ def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
 def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint64_mod"]
 def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
-@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
-def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
+@[deprecated UInt64.mod (since := "2024-09-23")]
+def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint64_land"]
 def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint64_lor"]
@@ -243,8 +243,8 @@ def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 @[extern "lean_usize_mod"]
 def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
-@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
-def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
+@[deprecated USize.mod (since := "2024-09-23")]
+def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.val n⟩
 @[extern "lean_usize_land"]
 def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_usize_lor"]
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index a3b4a281d9..cb625aa64d 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -1638,14 +1638,6 @@ static inline uint8_t lean_uint8_xor(uint8_t a, uint8_t b) { return a ^ b; }
 static inline uint8_t lean_uint8_shift_left(uint8_t a, uint8_t b) { return a << (b % 8); }
 static inline uint8_t lean_uint8_shift_right(uint8_t a, uint8_t b) { return a >> (b % 8); }
 static inline uint8_t lean_uint8_complement(uint8_t a) { return ~a; }
-static inline uint8_t lean_uint8_modn(uint8_t a1, b_lean_obj_arg a2) {
-    if (LEAN_LIKELY(lean_is_scalar(a2))) {
-        unsigned n2 = lean_unbox(a2);
-        return n2 == 0 ? a1 : a1 % n2;
-    } else {
-        return a1;
-    }
-}
 static inline uint8_t lean_uint8_log2(uint8_t a) {
     uint8_t res = 0;
     while (a >= 2) {
@@ -1682,14 +1674,6 @@ static inline uint16_t lean_uint16_xor(uint16_t a, uint16_t b) { return a ^ b; }
 static inline uint16_t lean_uint16_shift_left(uint16_t a, uint16_t b) { return a << (b % 16); }
 static inline uint16_t lean_uint16_shift_right(uint16_t a, uint16_t b) { return a >> (b % 16); }
 static inline uint16_t lean_uint16_complement(uint16_t a) { return ~a; }
-static inline uint16_t lean_uint16_modn(uint16_t a1, b_lean_obj_arg a2) {
-    if (LEAN_LIKELY(lean_is_scalar(a2))) {
-        unsigned n2 = lean_unbox(a2);
-        return n2 == 0 ? a1 : a1 % n2;
-    } else {
-        return a1;
-    }
-}
 static inline uint16_t lean_uint16_log2(uint16_t a) {
     uint16_t res = 0;
     while (a >= 2) {
@@ -1725,19 +1709,6 @@ static inline uint32_t lean_uint32_xor(uint32_t a, uint32_t b) { return a ^ b; }
 static inline uint32_t lean_uint32_shift_left(uint32_t a, uint32_t b) { return a << (b % 32); }
 static inline uint32_t lean_uint32_shift_right(uint32_t a, uint32_t b) { return a >> (b % 32); }
 static inline uint32_t lean_uint32_complement(uint32_t a) { return ~a; }
-LEAN_EXPORT uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
-static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) {
-    if (LEAN_LIKELY(lean_is_scalar(a2))) {
-        size_t n2 = lean_unbox(a2);
-        return n2 == 0 ? a1 : a1 % n2;
-    } else if (sizeof(void*) == 4) {
-        /* 32-bit */
-        return lean_uint32_big_modn(a1, a2);
-    } else {
-        /* 64-bit */
-        return a1;
-    }
-}
 static inline uint32_t lean_uint32_log2(uint32_t a) {
     uint32_t res = 0;
     while (a >= 2) {
@@ -1774,15 +1745,6 @@ static inline uint64_t lean_uint64_xor(uint64_t a, uint64_t b) { return a ^ b; }
 static inline uint64_t lean_uint64_shift_left(uint64_t a, uint64_t b) { return a << (b % 64); }
 static inline uint64_t lean_uint64_shift_right(uint64_t a, uint64_t b) { return a >> (b % 64); }
 static inline uint64_t lean_uint64_complement(uint64_t a) { return ~a; }
-LEAN_EXPORT uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
-static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
-    if (LEAN_LIKELY(lean_is_scalar(a2))) {
-        size_t n2 = lean_unbox(a2);
-        return n2 == 0 ? a1 : a1 % n2;
-    } else {
-        return lean_uint64_big_modn(a1, a2);
-    }
-}
 static inline uint64_t lean_uint64_log2(uint64_t a) {
     uint64_t res = 0;
     while (a >= 2) {
@@ -1820,15 +1782,6 @@ static inline size_t lean_usize_xor(size_t a, size_t b) { return a ^ b; }
 static inline size_t lean_usize_shift_left(size_t a, size_t b) { return a << (b %  (sizeof(size_t) * 8)); }
 static inline size_t lean_usize_shift_right(size_t a, size_t b) { return a >> (b % (sizeof(size_t) * 8)); }
 static inline size_t lean_usize_complement(size_t a) { return ~a; }
-LEAN_EXPORT size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
-static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
-    if (LEAN_LIKELY(lean_is_scalar(a2))) {
-        size_t n2 = lean_unbox(a2);
-        return n2 == 0 ? a1 : a1 % n2;
-    } else {
-        return lean_usize_big_modn(a1, a2);
-    }
-}
 static inline size_t lean_usize_log2(size_t a) {
     size_t res = 0;
     while (a >= 2) {
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 8d0f59c479..18eff602e9 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1547,20 +1547,10 @@ extern "C" LEAN_EXPORT uint32 lean_uint32_of_big_nat(b_obj_arg a) {
     return mpz_value(a).mod32();
 }
 
-extern "C" LEAN_EXPORT uint32 lean_uint32_big_modn(uint32 a1, b_lean_obj_arg a2) {
-    mpz const & m = mpz_value(a2);
-    return m.is_unsigned_int() ? a1 % m.get_unsigned_int() : a1;
-}
-
 extern "C" LEAN_EXPORT uint64 lean_uint64_of_big_nat(b_obj_arg a) {
     return mpz_value(a).mod64();
 }
 
-extern "C" LEAN_EXPORT uint64 lean_uint64_big_modn(uint64 a1, b_lean_obj_arg) {
-    // TODO(Leo)
-    return a1;
-}
-
 extern "C" LEAN_EXPORT uint64 lean_uint64_mix_hash(uint64 a1, uint64 a2) {
   return hash(a1, a2);
 }
@@ -1569,11 +1559,6 @@ extern "C" LEAN_EXPORT usize lean_usize_of_big_nat(b_obj_arg a) {
     return mpz_value(a).get_size_t();
 }
 
-extern "C" LEAN_EXPORT usize lean_usize_big_modn(usize a1, b_lean_obj_arg) {
-    // TODO(Leo)
-    return a1;
-}
-
 // =======================================
 // IntX
 
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 24ebe298a5..9610e1461d 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -384,7 +384,6 @@ inline uint8 uint8_sub(uint8 a1, uint8 a2) { return lean_uint8_sub(a1, a2); }
 inline uint8 uint8_mul(uint8 a1, uint8 a2) { return lean_uint8_mul(a1, a2); }
 inline uint8 uint8_div(uint8 a1, uint8 a2) { return lean_uint8_div(a1, a2); }
 inline uint8 uint8_mod(uint8 a1, uint8 a2) { return lean_uint8_mod(a1, a2); }
-inline uint8 uint8_modn(uint8 a1, b_obj_arg a2) { return lean_uint8_modn(a1, a2); }
 inline uint8 uint8_dec_eq(uint8 a1, uint8 a2) { return lean_uint8_dec_eq(a1, a2); }
 inline uint8 uint8_dec_lt(uint8 a1, uint8 a2) { return lean_uint8_dec_lt(a1, a2); }
 inline uint8 uint8_dec_le(uint8 a1, uint8 a2) { return lean_uint8_dec_le(a1, a2); }
@@ -398,7 +397,6 @@ inline uint16 uint16_sub(uint16 a1, uint16 a2) { return lean_uint16_sub(a1, a2);
 inline uint16 uint16_mul(uint16 a1, uint16 a2) { return lean_uint16_mul(a1, a2); }
 inline uint16 uint16_div(uint16 a1, uint16 a2) { return lean_uint16_div(a1, a2); }
 inline uint16 uint16_mod(uint16 a1, uint16 a2) { return lean_uint16_mod(a1, a2); }
-inline uint16 uint16_modn(uint16 a1, b_obj_arg a2) { return lean_uint16_modn(a1, a2); }
 inline uint16 uint16_dec_eq(uint16 a1, uint16 a2) { return lean_uint16_dec_eq(a1, a2); }
 inline uint16 uint16_dec_lt(uint16 a1, uint16 a2) { return lean_uint16_dec_lt(a1, a2); }
 inline uint16 uint16_dec_le(uint16 a1, uint16 a2) { return lean_uint16_dec_le(a1, a2); }
@@ -412,7 +410,6 @@ inline uint32 uint32_sub(uint32 a1, uint32 a2) { return lean_uint32_sub(a1, a2);
 inline uint32 uint32_mul(uint32 a1, uint32 a2) { return lean_uint32_mul(a1, a2); }
 inline uint32 uint32_div(uint32 a1, uint32 a2) { return lean_uint32_div(a1, a2); }
 inline uint32 uint32_mod(uint32 a1, uint32 a2) { return lean_uint32_mod(a1, a2); }
-inline uint32 uint32_modn(uint32 a1, b_obj_arg a2) { return lean_uint32_modn(a1, a2); }
 inline uint32 uint32_dec_eq(uint32 a1, uint32 a2) { return lean_uint32_dec_eq(a1, a2); }
 inline uint32 uint32_dec_lt(uint32 a1, uint32 a2) { return lean_uint32_dec_lt(a1, a2); }
 inline uint32 uint32_dec_le(uint32 a1, uint32 a2) { return lean_uint32_dec_le(a1, a2); }
@@ -425,7 +422,6 @@ inline uint64 uint64_sub(uint64 a1, uint64 a2) { return lean_uint64_sub(a1, a2);
 inline uint64 uint64_mul(uint64 a1, uint64 a2) { return lean_uint64_mul(a1, a2); }
 inline uint64 uint64_div(uint64 a1, uint64 a2) { return lean_uint64_div(a1, a2); }
 inline uint64 uint64_mod(uint64 a1, uint64 a2) { return lean_uint64_mod(a1, a2); }
-inline uint64 uint64_modn(uint64 a1, b_obj_arg a2) { return lean_uint64_modn(a1, a2); }
 inline uint64 uint64_dec_eq(uint64 a1, uint64 a2) { return lean_uint64_dec_eq(a1, a2); }
 inline uint64 uint64_dec_lt(uint64 a1, uint64 a2) { return lean_uint64_dec_lt(a1, a2); }
 inline uint64 uint64_dec_le(uint64 a1, uint64 a2) { return lean_uint64_dec_le(a1, a2); }
@@ -438,7 +434,6 @@ inline usize usize_sub(usize a1, usize a2) { return lean_usize_sub(a1, a2); }
 inline usize usize_mul(usize a1, usize a2) { return lean_usize_mul(a1, a2); }
 inline usize usize_div(usize a1, usize a2) { return lean_usize_div(a1, a2); }
 inline usize usize_mod(usize a1, usize a2) { return lean_usize_mod(a1, a2); }
-inline usize usize_modn(usize a1, b_obj_arg a2) { return lean_usize_modn(a1, a2); }
 inline usize usize_dec_eq(usize a1, usize a2) { return lean_usize_dec_eq(a1, a2); }
 inline usize usize_dec_lt(usize a1, usize a2) { return lean_usize_dec_lt(a1, a2); }
 inline usize usize_dec_le(usize a1, usize a2) { return lean_usize_dec_le(a1, a2); }
diff --git a/tests/lean/run/5818.lean b/tests/lean/run/5818.lean
new file mode 100644
index 0000000000..321a95daf6
--- /dev/null
+++ b/tests/lean/run/5818.lean
@@ -0,0 +1,2 @@
+theorem better2 : (UInt64.ofNat (2^64-1))%(2^63 : Nat) = 9223372036854775807 := by decide
+theorem better1 : (UInt64.ofNat (2^64-1))%(2^63 : Nat) = 9223372036854775807 := by native_decide