diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-14 15:46:03 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-17 14:50:14 -0400 |
| commit | 931b9f5007c33947adf3575a8d028841d2746546 (patch) | |
| tree | bfdd28f317c3d7da2d36b0efdb57f97de1823b60 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 7f828a9dc4d62ac3510e308e518ed5254f5db303 (diff) | |
Fix missing parenthesis
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index b8d49f3c1..b982b9a3e 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -747,7 +747,7 @@ Section CanonicalizationProofs. Lemma bound_after_third_loop : forall us, length us = length limb_widths -> - (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n])) -> + (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall n, 0 <= (carry_full (carry_full (carry_full us))) [n] < 2 ^ limb_widths [n]. Proof. |