diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-19 14:48:15 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-19 14:48:15 -0700 |
| commit | cdd44cf2718255b699ce6e77cfd4333a736ee804 (patch) | |
| tree | 9d1d998af183b3d4fa552b8d61b1501d40446862 /src | |
| parent | 51602bd1ccf7493e53f78afa958238cad14571f2 (diff) | |
Add another lemma to distr_length
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 6a8d4a8ff..45fea0356 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -788,7 +788,7 @@ Section carrying. Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. End carrying. -Hint Rewrite @length_carry_gen : distr_length. +Hint Rewrite @length_carry_gen @base_from_limb_widths_length : distr_length. Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length. Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default. Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. |