Slightly loosen freeze preconditions (in particular, I had failed to properly account for the case when which [n] and [pred n] are BOTH out of bounds in my statement of initial bounds)

1 files changed, 1 insertions, 1 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 89acd77f4..d2c73b57a 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -913,7 +913,7 @@ Section with_base.
     mkFreezePreconditions {
         lt_1_length_base : (1 < length base)%nat;
         int_width_pos : 0 < int_width;
-        int_width_compat : forall w, In w limb_widths -> w <= int_width;
+        int_width_compat : forall w, In w limb_widths -> w < int_width;
         c_pos : 0 < c;
         c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0;
         c_reduce2 : c < 2 ^ log_cap 0 - c;