diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-23 22:29:16 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-23 22:30:40 -0400 |
| commit | a4d5dfeb5e6b5eb9289ecb6643c4ba747dde97ca (patch) | |
| tree | 52f4e3cb2e2b25301df49d69307094ed6637c4a0 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | ce52efb544820b5ce88091cc68c94a3128c7bdd7 (diff) | |
Finished remaining admits in [freeze] proofs
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 7350fac76..5d7a1c24d 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -880,7 +880,7 @@ Section CanonicalizationProofs. | |- _ => apply conditional_subtract_lt_modulus | |- _ => apply conditional_subtract_modulus_preserves_bounded | |- bounded _ (carry_full _) => apply bounded_iff - | |- _ => solve [auto using length_to_list] + | |- _ => solve [auto using lt_1_length_limb_widths, length_carry_full, length_to_list] end. Qed. @@ -895,7 +895,7 @@ Section CanonicalizationProofs. | |- _ => rewrite Z.mod_add by (pose proof prime_modulus; prime_bound) | |- _ => rewrite to_list_from_list | |- _ => rewrite conditional_subtract_modulus_spec by - auto using length_carry_full, length_to_list + auto using lt_1_length_limb_widths, length_carry_full, length_to_list end. rewrite !decode_mod_Fdecode by auto using length_carry_full, length_to_list. cbv [carry_full]. |