Add FromNatural trait in Juvix.Builtin.V1

The FromNatural trait will be used for the Bytes type.

We want the following properties for Byte:

1. Values of the Bytes type to be assignable from a non-negative numeric
literal.
2. We don't want to implement + and * for it.

Currently, in order for a type to have property 1. it must have an
instance of `Natural` so property 2. can't be satisfied.

To solve this we split the `from-nat` builtin from the `Natural` trait
into a new trait `FromNatural`.

A coercion instance is defined between Natural and FromNatural so you
don't need to write instances for both traits.

For this PR the new `FromNatural` trait is unused. I will make the
changes to juvix-stdlib to use the new V2 modules when I incorporate
compiler changes for the Bytes type.

This change is backwards compatible for existing Juvix code so we don't
need to make a new Juvix.Builtin.V2 path in package-base.

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
+};

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};