Why not n elements?
n
https://gitlab.mpi-sws.org/FP/sra-gps/blob/master/coq/ra/examples/circ_buffer.v#L31