diff --git a/stage0/src/Init/Data/UInt.lean b/stage0/src/Init/Data/UInt.lean
index 62c4f7bc6d..16e41d00e2 100644
--- a/stage0/src/Init/Data/UInt.lean
+++ b/stage0/src/Init/Data/UInt.lean
@@ -362,3 +362,24 @@ instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 
 theorem USize.modnLt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u %ₙ m) < m
   | ⟨u⟩, h => Fin.modnLt u h
+
+theorem usizeSzEq : usizeSz = 4294967296 ∨ usizeSz = 18446744073709551616 :=
+  show (2 : Nat) ^ System.Platform.numBits = 4294967296 ∨ (2 : Nat) ^ System.Platform.numBits = 18446744073709551616 from
+  match System.Platform.numBits, System.Platform.numBitsEq with
+  | _, Or.inl rfl => Or.inl (decide! : (2 : Nat) ^ 32 = 4294967296)
+  | _, Or.inr rfl => Or.inr (decide! : (2 : Nat) ^ 64 = 18446744073709551616)
+
+@[extern "lean_usize_of_nat"]
+def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize := {
+  val := {
+    val  := n,
+    isLt := match usizeSz, usizeSzEq with
+      | _, Or.inl rfl => h
+      | _, Or.inr rfl => Nat.ltTrans h (decide! : Less 4294967296 18446744073709551616)
+  }
+}
+
+@[extern "lean_usize_of_nat"]
+def USize.ofNatCore (n : @& Nat) (h : n < usizeSz) : USize := {
+  val := { val := n, isLt := h }
+}
diff --git a/stage0/stdlib/Init/Data/UInt.c b/stage0/stdlib/Init/Data/UInt.c
index 0c6b294a1d..f92c2a6344 100644
--- a/stage0/stdlib/Init/Data/UInt.c
+++ b/stage0/stdlib/Init/Data/UInt.c
@@ -142,6 +142,7 @@ uint8_t l_UInt64_decLt(uint64_t, uint64_t);
 uint64_t l_Nat_toUInt64(lean_object*);
 lean_object* l_Init_Data_UInt___instance__11___boxed(lean_object*, lean_object*);
 uint8_t l_Init_Data_UInt___instance__64(size_t, size_t);
+size_t lean_usize_of_nat(lean_object*);
 lean_object* l_UInt64_mul___boxed(lean_object*, lean_object*);
 lean_object* l_Init_Data_UInt___instance__16;
 size_t l_USize_shiftLeft(size_t, size_t);
@@ -256,6 +257,7 @@ lean_object* lean_uint64_to_nat(uint64_t);
 lean_object* l_Init_Data_UInt___instance__9;
 lean_object* l_UInt16_mod___boxed(lean_object*, lean_object*);
 lean_object* l_USize_toUInt32___boxed(lean_object*);
+lean_object* l_USize_ofNatCore___boxed(lean_object*, lean_object*);
 uint32_t l_UInt32_lor(uint32_t, uint32_t);
 lean_object* l_Init_Data_UInt___instance__5;
 lean_object* l_UInt16_lor___boxed(lean_object*, lean_object*);
@@ -293,9 +295,11 @@ uint8_t l_UInt16_decLe(uint16_t, uint16_t);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 lean_object* l_Init_Data_UInt___instance__12___boxed(lean_object*, lean_object*);
 lean_object* l_Init_Data_UInt___instance__17;
+lean_object* l_USize_ofNat32___boxed(lean_object*, lean_object*);
 lean_object* l_Init_Data_UInt___instance__7___closed__1;
 lean_object* lean_uint32_to_nat(uint32_t);
 lean_object* l_Init_Data_UInt___instance__55___closed__1;
+size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Init_Data_UInt___instance__47;
 lean_object* l_UInt8_decEq___boxed(lean_object*, lean_object*);
 uint8_t l_Init_Data_UInt___instance__26(uint16_t, uint16_t);
@@ -2474,6 +2478,26 @@ x_6 = lean_box(x_5);
 return x_6;
 }
 }
+lean_object* l_USize_ofNat32___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+size_t x_3; lean_object* x_4; 
+x_3 = lean_usize_of_nat(x_1);
+lean_dec(x_1);
+x_4 = lean_box_usize(x_3);
+return x_4;
+}
+}
+lean_object* l_USize_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+size_t x_3; lean_object* x_4; 
+x_3 = lean_usize_of_nat(x_1);
+lean_dec(x_1);
+x_4 = lean_box_usize(x_3);
+return x_4;
+}
+}
 lean_object* initialize_Init_Data_Fin_Basic(lean_object*);
 lean_object* initialize_Init_System_Platform(lean_object*);
 static bool _G_initialized = false;