1 files changed, 2 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v
index c0078b117..504a26a0c 100644
--- a/src/PushButtonSynthesis/BarrettReduction.v
+++ b/src/PushButtonSynthesis/BarrettReduction.v
@@ -177,6 +177,7 @@ Section rbarrett_red.
                  | progress cbv [weight]
                  | rewrite mut_correct
                  | rewrite Mt_correct
+                 | rewrite UniformWeight.uweight_eq_alt'
                  | rewrite Z.pow_mul_r by lia ].
 
   Local Strategy -100 [barrett_red]. (* needed for making Qed not take forever *)
@@ -185,6 +186,7 @@ Section rbarrett_red.
   Proof using M curve_good.
     cbv [barrett_red_correct]; intros.
     assert (1 < machine_wordsize) by apply use_curve_good.
+    pose proof (Z.mod_pos_bound mu (2^machine_wordsize) ltac:(lia)).
     rewrite <-Fancy.fancy_reduce_correct with (mu := muLow + 2^machine_wordsize) (width:=machine_wordsize) (sz:=1%nat) (mut:=[muLow;1]) (Mt:=[M]) by solve_barrett_red_preconditions.
     prove_correctness' ltac:(fun _ => idtac) use_curve_good.
     { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower]. rewrite Bool.andb_true_iff, !Z.leb_le. lia. }