An iterated translation implies bijectivity

Prove that the function f: R-> R, with the property that $(f \circ f)(x) = x + 1$ is bijective.

Source: InternLM Lean-Workbook, record lean_workbook_2542 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.