diff options
Diffstat (limited to 'lib/Postorder.v')
| -rw-r--r-- | lib/Postorder.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Postorder.v b/lib/Postorder.v index 3181c4cc..eaeaea37 100644 --- a/lib/Postorder.v +++ b/lib/Postorder.v @@ -314,10 +314,10 @@ Proof. destruct (wrk s) as [ | [x succs] l]. discriminate. destruct succs as [ | y succs ]. - inv H. simpl. apply lex_ord_right. omega. + inv H. simpl. apply lex_ord_right. lia. destruct ((gr s)!y) as [succs'|] eqn:?. inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto. - inv H. simpl. apply lex_ord_right. omega. + inv H. simpl. apply lex_ord_right. lia. Qed. End POSTORDER. |