From 931b9f5007c33947adf3575a8d028841d2746546 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 14 Sep 2016 15:46:03 -0400 Subject: Fix missing parenthesis --- src/ModularArithmetic/ModularBaseSystemProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3