diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-15 16:41:01 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-15 16:41:01 -0400 |
| commit | c41720ac3b505fd067538e03a8504cfade377a32 (patch) | |
| tree | 93d547dcdeaab60dd2f1a80d257711d2cbbbe452 | |
| parent | e14cde53deba43a7744e4c9bd2a97a2a296b3d7b (diff) | |
Fix a changed case in the proof in loop.v
| -rw-r--r-- | src/Util/Loop.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Loop.v b/src/Util/Loop.v index 6c337d528..2ee90d11f 100644 --- a/src/Util/Loop.v +++ b/src/Util/Loop.v @@ -461,6 +461,7 @@ Section ScalarMult. cbv [ScalarMultBase]. eapply for_cps_ind with (invariant := fun i P => Geq P (smul (n_upto i) B )%Z). - intros; omega. + - omega. - intros; rewrite Z.ltb_lt in H; autorewrite with zsimplify; omega. - autorewrite with zsimplify. symmetry; eapply (scalarmult_0_l(add:=add)). - cbv [force_idZ id]; intros. clear H. |