diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 16:44:57 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 16:44:57 -0700 |
| commit | 2a14406a3d0ce41241471dbcb7cbd60fe2a66c59 (patch) | |
| tree | c67b2012a2afa95da8efb56a4611d9618f2d1e97 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 9b6a08343fd418296b069ead6fc4e879f8af0e7c (diff) | |
ext_base: now defined in terms of ext_limb_widths
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 227a3e77f..5d1becc00 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -132,7 +132,7 @@ Section PseudoMersenneProofs. (length us <= length base)%nat -> firstn (length us) base = firstn (length us) ext_base. Proof. - unfold ext_base; intros. + rewrite ext_base_alt; intros. rewrite firstn_app_inleft; auto; omega. Qed. Local Hint Immediate firstn_us_base_ext_base. @@ -184,7 +184,7 @@ Section PseudoMersenneProofs. Proof. intros. unfold BaseSystem.decode; rewrite <- mul_each_rep. - unfold ext_base. + rewrite ext_base_alt. replace (map (Z.mul (2 ^ k)) base) with (BaseSystem.mul_each (2 ^ k) base) by auto. rewrite base_mul_app. rewrite <- mul_each_rep; auto. |