diff options
Diffstat (limited to 'lib/Parmov.v')
| -rw-r--r-- | lib/Parmov.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v index db27e83f..f602bd60 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1106,7 +1106,7 @@ Lemma measure_decreasing_1: forall st st', dtransition st st' -> measure st' < measure st. Proof. - induction 1; repeat (simpl; rewrite List.app_length); simpl; omega. + induction 1; repeat (simpl; rewrite List.app_length); simpl; lia. Qed. Lemma measure_decreasing_2: |