Suppose we have a function that iterates an another function from some starting point. The function is defined as follows: $$iterate\ f\ x\ (n + 1) = f\ (iterate\ f\ x\ n)$$
Of course, with no iterations left we're constant. $$iterate\ f\ x\ 0 = x$$
Now suppose we find a fixed point after $m$ iterations. $$iterate\ f\ x\ m = x$$
And we would like to state that doing $n$ iterations with a fixpoint after $m$ iterations is the same as doing $n\ mod\ m$ iterations. $$iterate\ f\ x\ m = x \rightarrow \forall n, iterate\ f\ x\ n = iterate\ f\ x\ (n\ mod\ m)$$
I was trying to prove this by induction on $n$, with the inductive hypothesis: $$iterate\ f\ x\ k = iterate\ f\ x\ (k\ mod\ m)$$
However, I am stuck at transforming $$iterate\ f\ x\ (k + 1) = iterate\ f\ x\ ((k + 1)\ mod\ m)$$ to anything more usable. I have tried playing with the lhs, first using the definition of $iterate$, getting to lhs: $$f\ (itereate\ f\ x\ k)$$where I can use the inductive hypothesis to get: $$f\ (iterate\ f\ x\ (k\ mod\ m)) = iterate\ f\ x\ ((k + 1)\ mod\ m)$$ However, I still find the right hand side incredibly clumsy. I also tried proceeding by trichotomy $n < m \vee n = m \vee n > m$ where it's easy to show this holds for $n = m$ and $n < m$ from the definition of $iterate$, but I am stuck on the last case where we need to roll over the modulo.
Is induction not a good way to proceed here? If so, why? What am I missing here?
Here's what I'd do. I'll use the notation $f^{\circ n}(x)$ for your $iterate \; f \; x\; n$.
So you want to prove $f^{\circ n}(x) = x \Rightarrow f^{\circ m}(x) = f^{\circ m\,\mathrm{mod}(n)}(x)$, for $m \geq 0$.
If $0 \leq m < n$, this is obvious since then $m\,\mathrm{mod}n = m$ and obviously $f^{\circ m}(x) = f^{\circ m}(x)$. Also, the case where $m = n$ is the hypothesis. Hence you have $n+1$ base cases for $m = 0, 1, \dots, n$.
For the inductive case, let's prove $f^{\circ m+1}(x) = f^{\circ (m+1)\,\mathrm{mod}(n)}(x)$. Let's separate when $m+1\equiv 0 \mod n$ or not.
If $m+1\not\equiv0\mod n$, then $m+1\,\mathrm{mod}(n) = (m\,\mathrm{mod}(n)) + 1$. In that case $$f^{\circ m+1}(x) = f\left(f^{\circ m}(x)\right) = f\left(f^{\circ m\,\mathrm{mod}(n)}\right)(x) = f^{\circ (m\,\mathrm{mod}(n))+1}(x) = f^{\circ (m+1)\,\mathrm{mod}(n)}(x).$$
If $m + 1 \equiv 0 \mod n$, then $m = k \cdot n$ for some $k \geq 1$. Therefore
$$f^{\circ m+1}(x) = f^{\circ kn}(x) = f^{\circ n}\left(f^{\circ (k-1)n}(x)\right) = f^{\circ n}(x) = x =f^{\circ m\,\mathrm{mod}(n)}(x).$$
PS: Note that $f^{\circ0}$ is not constant, but the identity.