diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index bfb1963ff3..d3612f71bb 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -237,6 +237,10 @@ theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
           ...  =  a  + w1 : { symm L2 }
           ...  =  b       : Hw1
 
+set::opaque add true
+set::opaque mul true
+set::opaque le true
+set::opaque id true
 set::opaque ge true
 set::opaque lt true
 set::opaque gt true
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index c5df55a1e5..e07e061551 100644
Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ