Commit 2639ecba authored by Arthur Azevedo de Amorim's avatar Arthur Azevedo de Amorim
Browse files

Use lia instead of omega.

parent 41a6ec57
......@@ -50,14 +50,14 @@ Section symbol_ghost.
Proof.
rewrite -own_op.
apply own_update, auth_update_alloc, max_nat_local_update.
simpl. omega.
simpl. lia.
Qed.
Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
Proof.
iIntros "Hc Hs".
iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
iPureIntro. simpl in *. omega.
iPureIntro. simpl in *. lia.
Qed.
End symbol_ghost.
......
......@@ -50,14 +50,14 @@ Section symbol_ghost.
Proof.
rewrite -own_op.
apply own_update, auth_update_alloc, max_nat_local_update.
simpl. omega.
simpl. lia.
Qed.
Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
Proof.
iIntros "Hc Hs".
iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
iPureIntro. simpl in *. omega.
iPureIntro. simpl in *. lia.
Qed.
End symbol_ghost.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment