diff --git a/Clear/UInt256.lean b/Clear/UInt256.lean
index 390a6de..527f445 100644
--- a/Clear/UInt256.lean
+++ b/Clear/UInt256.lean
@@ -27,6 +27,21 @@ instance : NatCast UInt256 := ⟨Fin.ofNat⟩
 abbrev Nat.toUInt256 : ℕ → UInt256 := Fin.ofNat
 abbrev UInt8.toUInt256 (a : UInt8) : UInt256 := a.toNat.toUInt256
 
+def UInt256.top : ℕ := (⊤ : UInt256).val
+
+lemma UInt256.top_def : UInt256.top = 2 ^ 256 - 1 := by
+  unfold top
+  rw [Fin.top_eq_last]
+  simp
+
+lemma UInt256.top_def'
+  : UInt256.top = 115792089237316195423570985008687907853269984665640564039457584007913129639935 := by
+  rw [UInt256.top_def]; simp
+
+lemma UInt256.size_def
+  : UInt256.size = 115792089237316195423570985008687907853269984665640564039457584007913129639936 := by
+  unfold size; simp
+
 def Bool.toUInt256 (b : Bool) : UInt256 := if b then 1 else 0
 
 @[simp]