I am interested in how would one define `f` to the `n` in Coq:

![enter image description here](https://i.stack.imgur.com/MxDJQ.gif)

Basically, as an exercise, I would like to write this definition and then confirm that my
algorithm implements this specification. `Inductive` definition seems appropriate here, but I was not able to make it clean as above. What would be a clean Coq implementation of the above?