diff --git a/include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix b/include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix
new file mode 100644
index 0000000000..dea70e3ae2
--- /dev/null
+++ b/include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix
@@ -0,0 +1,10 @@
+module Juvix.Builtin.V1.Trait.FromNatural;
+
+import Juvix.Builtin.V1.Nat.Base open using {Nat};
+
+trait
+type FromNatural A :=
+  mkFromNatural {
+    builtin from-nat
+    fromNat : Nat -> A
+};
diff --git a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
index e17b3f51d0..ddf71c086f 100644
--- a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
+++ b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
@@ -2,6 +2,7 @@ module Juvix.Builtin.V1.Trait.Natural;
 
 import Juvix.Builtin.V1.Nat.Base open using {Nat};
 import Juvix.Builtin.V1.Fixity open;
+import Juvix.Builtin.V1.Trait.FromNatural open;
 
 trait
 type Natural A :=
@@ -12,8 +13,10 @@ type Natural A :=
     syntax operator * multiplicative;
     {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
     * : A -> A -> A;
-    builtin from-nat
     fromNat : Nat -> A
   };
 
 open Natural public;
+
+coercion instance
+FromNaturalNaturalI {A} {{N : Natural A}} : FromNatural A := mkFromNatural@{fromNat};