Cyclic successor is fixed-point-free

Cyclic successor on a finite set with at least two elements has no fixed point. For $l \ge 2$, the wraparound map $i \mapsto (i+1) \bmod l$ never fixes a point: a fixed point would force $(v+1) \bmod l = v$, impossible for $0 \le v < l$ with $l \ge 2$. This supplies the distinctness needed to read cycles as edge sets in the random graph model. Formalization Note Lean states it for the explicit cycSucc wraparound function.