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.