diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index c4d4ccca0..d1a6f6228 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -494,12 +494,12 @@ Section Multiplication. rewrite <- from_list_default_eq with (d := 0%Z). change (@from_list_default Z) with (@from_list_default_opt Z). apply f_equal. - rewrite ext_base_alt. + rewrite ext_base_alt by auto using limb_widths_pos with zarith. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. - rewrite k_subst. + fold k; rewrite k_subst. change @map with @map_opt. change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. |