I was fortunate that I have some experience proving things in Agda; it definitely helped me here.

For those who were struggling on getting Haskell to type check, I was able to get predictable results once I realized that any expression of (NextOdd m) or (NextEven m) was S^2 of some m, and that I also knew the parity of m by definition. Then I could just unfold the expressions in terms of n or m using the exact definitions for Mult and Add on paper for the cases I was considering, keeping in mind the nesting. Because it is trivial to determine the parity of all the terms in the expression, once I had the "shape" of the unfolded expressions on paper, it was just a matter of using the lemmas we already proved to recompose the expression in the form of the lemma analogs we defined for arithmetic, working from the innermost nested expression outward. Hope that made some sense. This was a fun kata, and bumped my score by 2 kyu.