You are missing one edge case (the statement is not true for n = 0, which probably you don't care). This my attempt at proving the theorem using Nat.mod.inductionOn.

Link to lean playground