diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 14:51:51 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 14:51:51 -0700 |
| commit | 29413b6c7d61993da6eaf9f5e6e9f227f4ec8709 (patch) | |
| tree | 0f221be468667a1086a3514970e28df2c2f5f069 /src/ModularArithmetic | |
| parent | 90c6403a50addd0cd0775aa45510e78505304017 (diff) | |
Make Pow2BaseProofs independent of the def of add_to_nth
Diffstat (limited to 'src/ModularArithmetic')
| -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 819a5adb5..6d6e3f530 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -575,7 +575,7 @@ Section carrying_helper. Lemma add_to_nth_sum : forall n x us, (n < length us \/ n >= length base)%nat -> BaseSystem.decode base (add_to_nth n x us) = x * nth_default 0 base n + BaseSystem.decode base us. - Proof. unfold add_to_nth; intros; rewrite set_nth_sum; try ring_simplify; auto. Qed. + Proof. intros; rewrite add_to_nth_set_nth, set_nth_sum; try ring_simplify; auto. Qed. Lemma add_to_nth_nth_default_full : forall n x l i d, nth_default d (add_to_nth n x l) i = |