Modular Concurrent Counter Module: The RA of the ILN does not match the one in Coq

The Modular Concurrent Counter presented in Section 13.1 used the RA `Auth((Q_{01} × N)_?)`, as opposed to `(Q_{01} × Ag Z), which is used in Coq (https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/lecture_notes/modular_incr.v).

This may be because Agree is not widely used (or even presented?) in the ILN.