diff --git a/.github/workflows/hacl-packages-create-branch.yml b/.github/workflows/hacl-packages-create-branch.yml
index cf42543816..cf13008bc8 100644
--- a/.github/workflows/hacl-packages-create-branch.yml
+++ b/.github/workflows/hacl-packages-create-branch.yml
@@ -34,7 +34,7 @@ jobs:
           git config --local user.name "Hacl Bot"
           git config --local user.email "hacl-star@mailo.com"
           git checkout -b $branch
-          git add src include
+          git add .
           git commit --allow-empty -m "[CI] update code"
           git push --force --set-upstream  origin $branch
       - name: comment pr
diff --git a/code/ed25519/Hacl.Spec.BignumQ.Lemmas.fst b/code/ed25519/Hacl.Spec.BignumQ.Lemmas.fst
index fe200b4689..ca3896faea 100644
--- a/code/ed25519/Hacl.Spec.BignumQ.Lemmas.fst
+++ b/code/ed25519/Hacl.Spec.BignumQ.Lemmas.fst
@@ -897,7 +897,7 @@ let aux (a b c:int)
   : Lemma (requires 0 <= b /\ c < a)
           (ensures 0 <= a + b -c) = ()
 
-#push-options "--z3rlimit 50 --fuel 0 --ifuel 0"
+#push-options "--z3rlimit 100 --fuel 0 --ifuel 0 --split_queries always"
 let lemma_barrett_reduce' x =
   assert_norm (S.q == 0x1000000000000000000000000000000014def9dea2f79cd65812631a5cf5d3ed);
   assert_norm (0x100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 == pow2 512);
@@ -951,7 +951,8 @@ let lemma_barrett_reduce' x =
          aux (pow2 264) r qml;
          assert (s >= 0);
          assert (s < 2 * l) by (
-           Tactics.set_rlimit 150;
+           Tactics.set_rlimit 250;
+           Tactics.set_options "--retry 5";
            ()
          );
          s
@@ -959,7 +960,8 @@ let lemma_barrett_reduce' x =
          let s = r - qml in
          assert (s >= 0);
          assert (s < 2 * l) by (
-           Tactics.set_rlimit 150;
+           Tactics.set_rlimit 250;
+           Tactics.set_options "--retry 5";
            ()
          );
          s
diff --git a/vale/code/lib/util/Vale.Def.Words.Seq.fst b/vale/code/lib/util/Vale.Def.Words.Seq.fst
index d6e62774f0..1c4d4158aa 100644
--- a/vale/code/lib/util/Vale.Def.Words.Seq.fst
+++ b/vale/code/lib/util/Vale.Def.Words.Seq.fst
@@ -52,12 +52,12 @@ let seq_four_to_seq_to_seq_four_BE (#a:Type) (x:seq a{length x % 4 == 0}) :
 
 unfold let pow2_24 = 16777216 //normalize_term (pow2 24)
 
-#reset-options "--z3rlimit 200 --using_facts_from 'Prims Vale.Def.Words_s'"
+#push-options "--z3rlimit 200 --using_facts_from 'Prims Vale.Def.Words_s'"
 let lemma_fundamental_div_mod_4 (x:nat32) :
   Lemma (x = x % pow2_8 + pow2_8 * ((x / pow2_8) % pow2_8) + pow2_16 * ((x / pow2_16) % pow2_8) + pow2_24 * ((x / pow2_24) % pow2_8))
   =
   ()
-#reset-options "--z3rlimit 30"
+#pop-options
 
 let four_to_nat_to_four_8 (x:natN (pow2_norm 32)) :
   Lemma (four_to_nat 8 (nat_to_four 8 x) == x)
@@ -80,29 +80,96 @@ let four_to_nat_to_four_8 (x:natN (pow2_norm 32)) :
   lemma_fundamental_div_mod_4 x;
   ()
 
-#reset-options "--z3rlimit 400 --using_facts_from 'Vale.Def.Words_s Prims'"
-let nat_to_four_to_nat (x:four (natN (pow2_norm 8))) :
-  Lemma (nat_to_four 8 (four_to_nat 8 x) == x)
-  [SMTPat (nat_to_four 8 (four_to_nat 8 x))]
+#push-options "--z3rlimit 20 --z3cliopt smt.arith.nl=true"
+(* Localized use of NL arith. The makefile passes the option to disable
+it in this file, so we reenable it here. *)
+let rec base_to_nat (base:pos) (cs : list (natN base)) : nat =
+  match cs with
+  | [] -> 0
+  | c :: cs' -> c + base_to_nat base cs' * base
+  (* NB: right-multiplying by base is a lot better than left-multiplying
+  since it more closely matches the lemmas in FStar.Math.Lemmas. *)
+#pop-options
+
+(* If two lists represent the same number, their heads must match,
+otherwise their modulus wrt the base would differ. *)
+let base_to_nat_inj_head (base:pos) (x y : list (natN base)) :
+  Lemma (requires base_to_nat base x == base_to_nat base y /\ Cons? x /\ Cons? y)
+        (ensures List.Tot.hd x == List.Tot.hd y)
+  =
+  match x, y with
+  | x1 :: xs, y1 :: ys ->
+    let x' = base_to_nat base x in
+    let y' = base_to_nat base y in
+    let open FStar.Math.Lemmas in
+    calc (==) {
+      x1 <: int;
+      == { small_mod x1 base }
+      x1 % base;
+      == { lemma_mod_plus x1 (base_to_nat base xs) base }
+      (x1 + base_to_nat base xs * base) % base;
+      == {}
+      x' % base;
+      == {}
+      y' % base;
+      == {}
+      (y1 + base_to_nat base ys * base) % base;
+      == { lemma_mod_plus y1 (base_to_nat base ys) base }
+      y1 % base;
+      == { small_mod y1 base }
+      y1;
+    }
+
+(* Generalizing the lemma above, if two lists represent the same number,
+and they have the same length, they must be the same list. The length requirement
+is due to the possibility of trailing zeroes. Another possibility is stating
+that one of them is a prefix of the other, which is enough for this module,
+even without stating that the "rest" is all zeroes. *)
+let rec base_to_nat_inj (base:pos) (x y : list (natN base)) :
+  Lemma (requires base_to_nat base x == base_to_nat base y /\ List.length x == List.length y)
+        (ensures x == y)
+  =
+  match x, y with
+  | [], [] -> ()
+  | x1 :: xs, y1 :: ys ->
+    base_to_nat_inj_head base x y;
+    let x' = base_to_nat base x in
+    let y' = base_to_nat base y in
+    let open FStar.Math.Lemmas in
+    calc (==) {
+      base_to_nat base xs * base;
+      == {}
+      x' - x1;
+      == {}
+      y' - y1;
+      == {}
+      base_to_nat base ys * base;
+    };
+    lemma_cancel_mul (base_to_nat base xs) (base_to_nat base ys) base;
+    assert (base_to_nat base xs == base_to_nat base ys);
+    base_to_nat_inj base xs ys
+
+#push-options "--fuel 4"
+(* Fuel needed to prove length equality *)
+let four_to_nat_inj (x y : four (natN 256)) :
+  Lemma (requires four_to_nat 8 x == four_to_nat 8 y)
+        (ensures x == y)
   =
-  let size = 8 in
-  let n1 = pow2_norm size in
-  let n2 = pow2_norm (2 * size) in
-  let n3 = pow2_norm (3 * size) in
-  let n4 = pow2_norm (4 * size) in
-  assert_norm (pow2 8 == 256);
-  assert_norm (pow2 16 == 0x10000);
-  assert_norm (pow2 24 == 0x1000000);
-  assert_norm (pow2 32 == 0x100000000);
-  let x' = four_to_nat 8 x in
-  assert_norm (nat_to_four 8 x' == Mkfour (x' % n1) ((x' / n1) % n1) ((x' / n2) % n1) ((x' / n3) % n1));
   let Mkfour x0 x1 x2 x3 = x in
-  let x' = x0 + x1 * n1 + x2 * n2 + x3 * n3 in
-  assert_norm (four_to_nat 8 x == int_to_natN n4 (x0 + x1 * n1 + x2 * n2 + x3 * n3));
-  lemma_fundamental_div_mod_4 x';
+  let Mkfour y0 y1 y2 y3 = y in
+  assert_norm (four_to_nat 8 (Mkfour x0 x1 x2 x3) == base_to_nat 256 [x0; x1; x2; x3]);
+  assert_norm (four_to_nat 8 (Mkfour y0 y1 y2 y3) == base_to_nat 256 [y0; y1; y2; y3]);
+  base_to_nat_inj 256 [x0; x1; x2; x3] [y0; y1; y2; y3];
   ()
+#pop-options
+
+let nat_to_four_to_nat (x:four (natN 256)) :
+  Lemma (nat_to_four 8 (four_to_nat 8 x) == x)
+  [SMTPat (nat_to_four 8 (four_to_nat 8 x))]
+  =
+  four_to_nat_to_four_8 (four_to_nat 8 x);
+  four_to_nat_inj (nat_to_four 8 (four_to_nat 8 x)) x
 
-#reset-options
 let four_to_seq_to_four_LE (#a:Type) (x:seq4 a) :
   Lemma (four_to_seq_LE (seq_to_four_LE x) == x)
   =