Avoid using Arith libraries deprecated in v8.16

Coq v8.16 will deprecate several libraries in Arith (see https://github.com/coq/coq/pull/14736). This results in warnings like:

File "./theories/numbers.v", line 1374, characters 13-23:
Warning: Notation plus_assoc is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
[deprecated-syntactic-definition,deprecated]
File "./theories/list.v", line 1207, characters 29-47:
Warning: Notation Min.min_idempotent is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_id instead.
[deprecated-syntactic-definition,deprecated]

These changes seem to be backwards-compatible to Coq 8.11 so we might as well fix them now. In several cases the recommended fix is incorrect because it isn't the same lemma (for example, minus_plus has no replacement lemma, at least with the current imports); in those cases I changed the proof script to use replace and lia rather than introduce a lemma identical to the old one to continue using rewrite.

Looking at the diff, it seems to me like it'd be worth having a lemma for minus_plus in std++. That's less verbose than all these replaces.

I'm pretty sure you mean le_plus_minus, but in any case I added both and used them instead.

added 1 commit

• 0210d4c9 - Avoid using Arith libraries deprecated in v8.16

Compare with previous version

mentioned in merge request iris!765 (merged)

added 1 commit

• 17190de7 - Use coqdoc syntax

Compare with previous version

resolved all threads

LGTM.

I think it's a bit weird that Coq's PeanoNat.Nat does not have these lemmas for minus, the ones it has are less useful. Maybe a Coq issue would be useful to report that?

At either rate, I'm happy with adding them to std++.

This probably needs a changelog.

resolved all threads

merged

mentioned in commit 9135fcfe